Michael C Case

US Patent:

8146034, Mar 27, 2012

Filed:

Apr 30, 2010

Appl. No.:

12/771677

Inventors:

Jason R. Baumgartner - Austin TX, US
Michael L. Case - Pflugerville TX, US
Robert L. Kanzelman - Rochester MN, US
Hari Mony - Austin TX, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 17/50

US Classification:

716107

Abstract:

A mechanism is provided for efficient redundancy identification, redundancy removal, and sequential equivalence checking with designs including memory arrays. The mechanism includes an array merging component to optimally merge an array output such that if the address is out-of-bounds or the port is not asserted, the array output is converted to a random output. The mechanism also includes a component for determining the equivalence of enabled array outputs rather than the array outputs directly and creating an enabled array output. The mechanism also includes a component that precludes potentially-redundant array cells from participating in the sequential redundancy removal determination. This component first checks for compatibility of the corresponding arrays, then the corresponding read port enables and addresses, then the corresponding initial values, and finally checking that writes to the corresponding columns yield a compatible set of values.

US Patent:

8171437, May 1, 2012

Filed:

Mar 25, 2009

Appl. No.:

12/410968

Inventors:

Jason R. Baumgartner - Austin TX, US
Michael L. Case - Pflugerville TX, US
Geert Janssen - Putnam Valley NY, US
Hari Mony - Austin TX, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 9/45

US Classification:

716103, 716106, 716107, 716108, 716111, 716113

Abstract:

A method, system and computer program product for X-Saturated ternary simulation based reduction. An X-Saturated ternary simulation (XSTS) utility, which executes on a computer system, receives design information, where the design information includes a netlist. The XSTS utility initializes one or more data structures and/or variables and simulates, in a ternary fashion, the netlist at a time value by applying logical X values to all RANDOM gates of the netlist and to registers marked X_SATURATED. For each register of the netlist XSTS utility: determines whether or not the register departs from its expected prefix behavior, and if the register departs from its expected prefix behavior, the register is marked as X_SATURATED and the current state is updated with an X value upon the register. XSTS utility can store the current state in a data structure and can use the information from the data structure to simplify the design.

US Patent:

8181131, May 15, 2012

Filed:

Apr 30, 2010

Appl. No.:

12/771613

Inventors:

Jason R. Baumgartner - Austin TX, US
Michael L. Case - Pflugerville TX, US
Robert L. Kanzelman - Rochester MN, US
Hari Mony - Austin TX, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 9/455
G06F 17/50
G06F 9/45

US Classification:

716103, 716106, 716111

Abstract:

A mechanism is provided for increasing the scalability of formal verification solutions through enabling the use of input reparameterization on logic models that include memory arrays. A pre-processing mechanism enables the selection of a cut-based design partition which enables optimal reductions though input reparameterization given a netlist with constraints. A post-processing mechanism next prevents input reparameterization from creating topologically inconsistent models in the presence of arrays. Additionally, this technique may be used to rectify inconsistent topologies that may arise when reparameterizing even netlists without arrays, namely false sequential dependencies across initialization constructs. Furthermore, a mechanism is provided to undo the effects of memory array based input reparameterization on verification results.

US Patent:

8181134, May 15, 2012

Filed:

Oct 16, 2009

Appl. No.:

12/580373

Inventors:

Jason R. Baumgartner - Austin TX, US
Michael L. Case - Pflugerville TX, US
Hari Mony - Austin TX, US
Jun Sawada - Austin TX, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 17/50

US Classification:

716107, 716103, 716104, 716111, 703 16

Abstract:

A technique for conditional sequential equivalence checking of logic designs embodied in netlists includes creating an equivalence-checking netlist over a first netlist and a second netlist. The conditional sequential equivalence checking includes conditions under which equivalences of the first and second netlists are checked. The technique derives a set of candidate conditional equivalence invariants for each correlated gate in a correlated gate pair set and attempts to prove that each candidate conditional equivalence invariant in the set of candidate conditional equivalence invariants is accurate. The candidate conditional equivalence invariants that cannot be proven accurate are removed from the set of candidate conditional equivalence invariants. The candidate conditional equivalence invariants that have been proven accurate are recorded as a set of conditional equivalence invariants. Finally, the conditional sequential equivalence checking of the equivalence-checking netlist is completed using the set of conditional equivalence invariants that are recorded.

US Patent:

8201115, Jun 12, 2012

Filed:

Aug 14, 2008

Appl. No.:

12/191635

Inventors:

Jason R. Baumgartner - Austin TX, US
Michael L. Case - Pflugerville TX, US
Hari Mony - Austin TX, US
Viresh Paruthi - Austin TX, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 17/50
G06F 9/455

US Classification:

716106, 716103, 716107, 716110, 716111, 716112, 716136, 703 13, 703 14

Abstract:

A method, system, and computer program product for reducing the size of a logic network design, prior to verification of the logic network design. The method includes eliminating registers to reduce the size of the logic network design; thereby, increasing the speed and functionality of the verification process, and decreasing the size of the logic network design. The system identifies one or more compatible resubstitutions of a selected register, wherein the compatible resubstitution expresses the selected register as one or more pre-existing registers of fixed initial state. The resubstitutions are refined utilizing design invariants. When one more resubstitutions are preformed, the system eliminates the selected registers to reduce the size of the logic network design. As a result of the resubstitution process, a logic network design of reduced size is generated.

US Patent:

8201117, Jun 12, 2012

Filed:

Jan 22, 2009

Appl. No.:

12/357907

Inventors:

Jason R. Baumgartner - Austin TX, US
Michael L. Case - Pflugerville TX, US
Geert Janssen - Putnam County NY, US
Hari Mony - Austin TX, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 17/50
G06F 9/455

US Classification:

716107

Abstract:

A method, system and computer program product for integrating implication-based analysis and equivalent gate analysis to maintain transitive reduction in an implication graph over a sequence of graph operations. One or more gates of a design are identified that are equivalent in all reachable states. Equivalent gates are assigned to an equivalence class when all gates within the equivalence class are equal. During the implication-based analysis the system determines when one or more implication paths are associated with the one or more equivalence classes, and an implication is generated at the implication path associated with the equivalence classes. A transitively reduced graph is received depicting the implications and equivalence classes of the design. When one or more operations are assigned to the transitively reduced graph, the graph is automatically adjusted to maintain transitive reduction.

US Patent:

8245166, Aug 14, 2012

Filed:

Aug 31, 2010

Appl. No.:

12/871962

Inventors:

Jason R. Baumgartner - Austin TX, US
Michael L. Case - Pflugerville TX, US
Robert L. Kanzelman - Rochester MN, US
Hari Mony - Austin TX, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 17/50

US Classification:

716111

Abstract:

Mechanisms are provided for refining an abstraction of a netlist for verification or synthesis of an integrated circuit design. The mechanisms receive an abstracted netlist corresponding to an original netlist of the integrated circuit design. The mechanisms determine elements already present in the abstracted netlist and refine the abstracted netlist by expanding the abstracted netlist to include additional elements that are correlated with the elements already present in the abstracted netlist to thereby generate a refined abstracted netlist. In addition, the mechanisms utilize the refined abstracted netlist to perform at least one of verification or synthesis of the integrated circuit design.

US Patent:

8291359, Oct 16, 2012

Filed:

May 7, 2010

Appl. No.:

12/775633

Inventors:

Jason R. Baumgartner - Austin TX, US
Michael L. Case - Pflugerville TX, US
Robert L. Kanzelman - Rochester MN, US
Hari Mony - Austin TX, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 17/50

US Classification:

716103, 716104, 716107, 716111, 716132

Abstract:

Mechanisms are provided in a design environment for array concatenation. The design environment comprises one mechanism to concatenate arrays with enable- and address-compatible ports, thereby reducing the number of arrays in a netlist. The design environment comprises another mechanism to migrate read ports from one array to another based upon compatible enable-, address-, and data-compatible write ports, thereby reducing the number of arrays in a netlist. The design environment comprises yet another mechanism to eliminate unnecessary arrays.