Method and system for design verification using proof-based abstraction
AssigneeCadence Design Systems, Inc.
InventorsKenneth L. McMillan, Nina Amla
Life of this patent
Estimating the term…
Abstract
A design verifier includes a bounded model checker, an abstractor and an unbounded model checker. The bounded model checker verifies a property to a depth K and either finds a counterexample, or generates a proof in the form of a directed acyclic graph. If no counterexample is found, the abstractor generates an abstracted design description using a proof generated by the bounded model checker. The unbounded model checker verifies the property of the abstracted design description. If a counterexample is found, the bounded model checker increases K and verifies the property to the new larger depth. If no counterexample is found, the design is verified.
Claims28
A method for verifying a property of a design of a system, the method comprising:
- performing bounded model checking on a design description for the system to a depth of K steps, the design description including a plurality of constraints referring to states of components within the system, each constraint including at least one variable;
- abstracting the design description responsive to a proof generated in performing the bounded model checking when no counterexample of depth K is found in performing the bounded model checking, the proof including at least one inference derived from a constraint of the plurality of constraints, each inference including at least one variable;
- performing an unbounded model checking on the abstracted design description;
- and
- outputting a result response to the unbounded model checking.
An apparatus for verifying a property of a circuit design for a system, the apparatus comprising:
- one or more processors executing machine readable instructions stored in a machine readable medium to verify the property of the circuit design, including:
- instructions for performing bounded model checking on a design description for the system to a depth of K steps, the design description including a plurality of constraints referring to states of components within the system, each constraint including at least one variable;
- instructions for abstracting the design description responsive to a proof generated in performing the bounded model checking when no counterexample of depth K is found in performing the bounded model checking, the proof including at least one inference derived from a constraint of the plurality of constraints, each inference including at least one variable;
- instructions for performing unbounded model checking on the abstracted design description;
- and
- instructions for outputting a result responsive to the unbounded model checking.
A machine readable storage media having stored therein instructions that when executed by a machine causes the machine to perform operations comprising:
- performing bounded model checking on a design description of a system to a depth of K steps, the design description including a plurality of constraints referring to states of components within the system, each constraint including at least one variable;
- abstracting the design description responsive to a proof generated in performing the bounded model checking when no counterexample of depth K is found in performing the bounded model checking, the proof including at least one inference derived from a constraint of the plurality of constraints, each inference including at least one variable;
- performing an unbounded model checking on the abstracted design description;
- and
- outputting a result responsive to the unbounded model checking.
A machine-readable media having machine-executable modules stored therein which when executed causes a machine to perform operations for verifying a property of a design for a system, the modules comprising:
- a bounded model checker having a proof generator to verify a property of a design description to a depth of K steps, the design description including a plurality of constraints referring to states of components within the system, each constraint including at least one variable;
- and
- an abstractor to provide an abstracted design description related to the design description using on a proof generated by the proof generator when the bounded model checker finds no counterexample in K steps, the proof including at least one inference derived from a constraint of the plurality of constraints, each inference including at least one variable;
- and
- an unbounded model checker to verify the property of the abstracted design description, wherein the unbounded model checker is to output a result.
Dependencies are inferred from the claim text.