International Business Machines Corporation

Jiazhao Xu

Viresh Paruthi

Jason Raymond Baumgartner

Hari Mony

Christian Jacobi

Geert Janssen

Kai Oliver Weber

Paul Joseph Roessler

Ohad Shacham

Mark A Williams

A technique for verification of a logic design using a liveness-to-safety conversion includes assigning liveness gates for liveness properties of a netlist and assigning a single loop gate to provide a loop signal for the liveness gates. Assertion of the single loop gate is prevented when none of the liveness gates are asserted. A first state of the netlist is sampled and the sampled first state provides an initial state for a first behavioral loop for at least one of the liveness gates following the assertion of the single loop gate. The sampled first state of the first behavioral loop is compared with a later state of the first behavioral loop to determine if the sampled first state is repeated. A liveness violation is returned when the sampled first state is repeated and an associated one of the liveness gates remains asserted for a duration of the first behavioral loop.

Verification techniques for liveness checking of logic designs

Methods and systems are provided for dynamically generating a hint set for enhanced reachability analysis in a sequential circuitry design that is represented by a Binary Decision Diagram (BDD). After determining a ranking of the BDD variables, they are sorted in the order of the ranking. The ranking is used to select some of the variables for use in creating hints for more efficiently performing the reachability analysis in a creating an equivalent sequential circuitry design.

Method and system for dynamic automated hint generation for enhanced reachability analysis

A method for generating a constraint for generating a constraint for use in the verification of an integrated circuit design includes identifying a target in a netlist (N) of the design and creating an overapproximate abstraction (N') of the netlist. A space state (S&#x2032;) is created by enumerating the states of N&#x2032; from which the identified target may be asserted. A constraint space C&#x2032; is then derived from the state space S&#x2032;, where C&#x2032; is the logical complement of S&#x2032;. The process is repeated for multiple selected targets and the constraint spaces from each iteration are logically ANDed. Creating an overapproximate abstraction may include replacing a sequential gate with a random gate. Identifying a sequential gate may include selecting a target in the netlist, performing underapproximate verification of the target, and, if a spurious failure occurs, selecting a gate further down the fanin chain of the currently selected gate.

Using constraints in design verification

A method, system and computer program product for building decision diagrams efficiently in a structural network representation of a digital circuit using a dynamic resource constrained and interleaved depth-first-search and modified breadth-first-search schedule is disclosed. The method includes setting a first size limit for a first set of one or more m-ary decision representations describing a logic function and setting a second size limit for a second set of one or more m-ary decision representations describing a logic function. The first set of m-ary decision representations of the logic function is then built with one of the set of a depth-first technique or a breadth-first technique until the first size limit is reached, and a second set of m-ary decision representations of the logic function is built with the other technique until the second size limit is reached. In response to determining that a union of first set and the second set of m-ary decision representations do not describe the logic function, the first and second size limits are increased, and the steps of building the first and second set are repeated. In response to determining that the union of the first set of m-ary decision representations and the second set of m-ary decision representations describe the logic function, the union is reported.

System for building binary decision diagrams efficiently in a structural network representation of a digital circuit

Building binary decision diagrams efficiently in a structural network representation of a digital circuit

A method, system and computer program product for verifying that a design conforms to a desired property is disclosed. The method comprises receiving a design, a first initial state of the design, and a property for verification with respect to the design. The first initial state of the design is expanded to create a superset of the first initial state containing one or more states reachable from the first initial state of the design. A superset is synthesized to define a second initial state of the design. Application of the superset to the design is overapproximated through cutpoint insertion into the superset to obtain a modified superset, and the property is verified with reference to the modified superset.

Computer program product for verification using reachability overapproximation

A method, apparatus and computer-readable medium for conjunctive binary decision diagram building and variable quantification using case-splitting are presented. A BDD building program builds a BDD for at least one node in a netlist graph representation of a circuit design. One or more variables are selected for case-splitting. The variable is set to a constant logical value and then the other. A BDD is built for each case. The program determines whether the variable is scheduled to be quantified out. If so, the program combines the BDDs for each case according to whether the quantification is existential or universal. If the variable is not scheduled to be quantified, the program combines the BDDs for each case so that the variable is introduced back into the resulting BDD, which has a reduced number of peak live nodes.

Conjunctive BDD building and variable quantification using case-splitting

System for verification using reachability overapproximation

A method for generating a constraint for use in the verification of an integrated circuit design includes identifying a target in a netlist (N) of the design and creating an overapproximate abstraction (N') of the netlist. A space state (S&#x2032;) is created by enumerating the states of N&#x2032; from which the identified target may be asserted. A constraint space C&#x2032; is then derived from the state space S&#x2032;, where C&#x2032; is the logical complement of S&#x2032;. The process is repeated for multiple selected targets and the constraint spaces from each iteration are logically ANDed. Creating an overapproximate abstraction may include replacing a sequential gate with a random gate. Identifying a sequential gate may include selecting a target in the netlist, performing underapproximate verification of the target, and, if a spurious failure occurs, selecting a gate further down the fanin chain of the currently selected gate.

Method and system for building binary decision diagrams efficiently in a structural network representation of a digital circuit

Method for verification using reachability overapproximation

A method, system and computer program product for performing retiming in the presence of constraints are disclosed. The method comprises receiving an initial design containing one or more targets and one or more constraints and enumerating the one or more constraints and the one or more targets into a retiming gate set. A retiming graph is constructed from the initial design, and a retiming solution is obtained on the retiming graph. The retiming solution is normalized. One or more retiming lags from the retiming graph are propagated to the initial design, and the initial design is verified by using a constraint-satisfying analysis to determine whether the one or more targets may be hit while the one or more constraints are satisfied.

Growing community of inventors

Mount Kisco, NY, United States of America

Jiazhao Xu