Robert L Kanzelman

6745377, Jun 1, 2004

Apr 4, 2002

10/116584

Jason Raymond Baumgartner - Austin TX
Robert Lowell Kanzelman - Rochester MN
Wolfgang Roesner - Austin TX

International Business Machines Corporation - Armonk NY

G06F 1750

716 6, 716 3, 716 7, 716 2, 703 16

An apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs is provided. With the apparatus and method, latches are âcolored,â i. e. classified into different types, based on information obtained from a clock tree of the circuit design. Clock tree primitives contain sufficient information to taxonomize the clocks into their respective phases and identify which latches are gated latches. In coloring the latches, gated latches are replaced in the circuit design with a free running clock, a multiplexor, and a sequence of L1 to Ln latches to provide a feedback path via the data path. This allows the gated latch to be phase abstracted without losing the âgatedâ functionality of the gated latch in the resulting trace. Once the latches are colored in this way, phase abstraction is performed on the colored circuit design. The phase abstracted netlist is then subjected to verification and a trace is produced.

6748573, Jun 8, 2004

Apr 4, 2002

10/116583

Jason Raymond Baumgartner - Austin TX
Robert Lowell Kanzelman - Rochester MN
Wolfgang Roesner - Austin TX

International Business Machines Corporation - Armonk NY

G06F 1750

716 5, 716 2, 716 3, 716 7, 703 15

An apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs is provided. With the apparatus and method, latches are âcolored,â i. e. classified into different types, based on information obtained from a clock tree of the circuit design. Clock tree primitives contain sufficient information to taxonomize the clocks into their respective phases and identify which latches are gated latches. In coloring the latches, gated latches are replaced in the circuit design with a free running clock, a multiplexor, and a sequence of L to Ln latches to provide a feedback path via the data path. This allows the gated latch to be phase abstracted without losing the âgatedâ functionality of the gated latch in the resulting trace. Once the latches are colored in this way, phase abstraction is performed on the colored circuit design. The phase abstracted netlist is then subjected to verification and a trace is produced.

6763505, Jul 13, 2004

Apr 4, 2002

10/116607

Jason Raymond Baumgartner - Austin TX
Robert Lowell Kanzelman - Rochester MN
Wolfgang Roesner - Austin TX

International Business Machines Corporation - Armonk NY

G06F 1750

716 5, 716 4, 716 6, 716 1, 716 3

An apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs is provided. With the apparatus and method, latches are âcolored,â i. e. classified into different types, based on information obtained from a clock tree of the circuit design. Clock tree primitives contain sufficient information to taxonomize the clocks into their respective phases and identify which latches are gated latches. In coloring the latches, gated latches are replaced in the circuit design with a free running clock, a multiplexor, and a sequence of L1 to Ln latches to provide a feedback path via the data path. This allows the gated latch to be phase abstracted without losing the âgatedâ functionality of the gated latch in the resulting trace. Once the latches are colored in this way, phase abstraction is performed on the colored circuit design. The phase abstracted netlist is then subjected to verification and a trace is produced.

7093218, Aug 15, 2006

Feb 19, 2004

10/782673

Jason Raymond Baumgartner - Austin TX, US
Robert Lowell Kanzelman - Rochester MN, US
Hari Mony - Austin TX, US
Viresh Paruthi - Austin TX, US

International Business Machines Corporation - Armonk NY

G06F 17/50
G06F 19/00

716 5, 716 7, 716 2, 716 3, 703 16

A design verification system includes a first verification engine to model the operation of a first design of an integrated circuit to obtain verification results including the model's adherence to a property during N time steps of its operation, proofs that one or more verification targets can be reached, and verification coverage results for targets that are not reached. A correspondence engine determines the functional correspondence between the first design and a second design of the integrated circuit. Functional correspondence, if demonstrated, enables reuse of the first engine's verification results to reduce resources expended during subsequent analysis of the second design. The correspondence determination may be simplified using a composite model of the integrated circuit having “implies” logic in lieu of “EXOR” logic. The implies logic indicates conditions in which a node in the second design achieves a state that is contrary to the verification results for the first design.

7210109, Apr 24, 2007

Jun 24, 2004

10/875476

Kenneth Michael Caron - Rochester MN, US
Robert Lowell Kanzelman - Rochester MN, US
Scott Henry Mack - Rochester MN, US
Lance Gordon Thompson - Rochester MN, US
Mark Allen Williams - Pleasant Valley NY, US

International Business Machines Corporation - Armonk NY

G07F 17/50

716 4, 716 3, 716 5, 716 6, 716 11, 714724, 714726, 714728

A method, apparatus, system, and signal-bearing medium that in an embodiment apply a latch behavior to a first and second netlist, where the latch behavior exhibits transparent behavior. Flush enabling conditions are applied to the first netlist and a second netlist. For each latch in a first scan chain in the first netlist, a corresponding latch in the second netlist is found. Cones of logic are then extracted from the latches under the constraints enabling the flush operation, and the cones of logic are compared for functional equivalence. If all the cones are functionally equivalent, then the flush reset states of the netlists are functionally equivalent. If at least one of the cones is not functionally equivalent, then the flush reset states of the two netlists are not equivalent.

7260799, Aug 21, 2007

Feb 10, 2005

11/054904

Jason Raymond Baumgartner - Austin TX, US
Robert Lowell Kanzelman - Rochester MN, US
Hari Mony - Austin TX, US
Viresh Paruthi - Austin TX, US

International Business Machines Corporation - Armonk NY

G06F 17/50

716 5, 716 4, 703 14, 703 15

A verification method foe an integrated circuit includes identifying an equivalence class including a set of candidate gates suspected of exhibiting equivalent behavior and identifying one of the candidate gates as a representative gate for the equivalence class. Equivalence gates of an XOR gate are sourced by the representative gate and a candidate gate. A speculatively reduced netlist is generated by replacing the representative gate as the source gate for edges sourced by a candidate gate in the original design. The speculatively reduced netlist is then used either to verify formally the equivalence of the gates by applying a plurality of transformation engines to the speculatively reduced netlist or to perform incomplete search and, if none of the equivalence gates is asserted during the incomplete search, any verification results derived from the incomplete search can be applied to the original model.

7266795, Sep 4, 2007

Mar 17, 2005

11/082699

Jason Raymond Baumgartner - Austin TX, US
Robert Lowell Kanzelman - Rochester MN, US
Hari Mony - Austin TX, US
Viresh Paruthi - Austin TX, US

International Business Machines Corporation - Armonk NY

G06F 17/50

716 5, 716 4, 716 17

A system and method for implementing a verification system. Included is a first set of verification engines for attempting to solve a verification problem. At least one of the first set of verification engines divides the verification problem into a set of partitions and passes at least one of the set of partitions to a second set of verification engines. Each one of the set of partitions may be passed to a distinctly separate verification engine. A system framework is configured to communicate with an application program and further configured to instantiate at least one verification engine in a user-defined sequence. Included within at least one of the first set of verification engines is a means for communicating verification information to the second set of verification engines.

7315996, Jan 1, 2008

Sep 22, 2005

11/232764

Jason R. Baumgartner - Austin TX, US
Robert L. Kanzelman - Rochester MN, US
Hari Mony - Austin TX, US
Viresh Paruthi - Austin TX, US

International Business Machines Corporation - Armonk NY

G06F 17/50

716 5, 716 3, 716 4

A method for performing verification is disclosed. The method includes selecting a first computer-design constraint for simplification and applying structural reparameterization to simplify the first computer-design constraint. In response to determining that the first computer-design constraint is not eliminated, the first computer-design constraint is set equal to a dead-end state of the constraint. A structural preimage of the first computer-design constraint is created, in response to determining that a combination of a target and the dead-end state of the first computer-design constraint is equal to a combination of the target and the structural preimage of the first computer-design constraint, the first computer-design constraint is set equal to the structural preimage.