Kenneth E Mcmillan

6944838, Sep 13, 2005

Feb 3, 2003

10/357657

Kenneth L. McMillan - Berkeley CA, US

Cadence Design Systems, Inc. - San Jose CA

G06F009/45

716 5, 716 4, 703 2, 703 14

A design verifier includes a bounded model checker, a proof partitioner and a fixed-point detector. 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 a counterexample is found, the bounded model checker selectively increases K and verifies the property to the new larger depth using the original constraints. If no counterexample is found, the proof partitioner provides an over-approximation of the states reachable in one or more steps using a proof generated by the bounded model checker. The fixed-point detector detects whether the over-approximation is at a fixed point. If the over-approximation is at a fixed-point, the design is verified. If the over-approximation is not at a fixed point, the bounded model checker can iteratively use over-approximations as a constraint and verify the property to a depth K.

7406405, Jul 29, 2008

Feb 3, 2003

10/357585

Kenneth L. McMillan - Berkeley CA, US
Nina Amla - Hoboken NJ, US

Cadence Design Systems, Inc. - San Jose CA

G06F 17/10
G06F 9/45

703 2, 703 14, 716 4, 716 5

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.

7661082, Feb 9, 2010

Mar 28, 2007

11/692802

Kenneth L. McMillan - Berkeley CA, US
Nina Amla - Hoboken NJ, US

Cadence Design Systems, Inc. - San Jose CA

G06F 17/50
G06F 9/45

716 5, 716 1, 716 2, 716 3, 716 4, 716 18, 703 13, 703 14

An apparatus and methods for the verification of digital design descriptions are provided. In an exemplary embodiment, a method of verifying a property in a digital design description is provided. The method includes deriving an abstraction of the digital design description, determining a counterexample by an approximate reachable state computation, justifying the counterexample, determining a justification frontier, updating the abstraction from the justification frontier, and producing a verification result for the digital design description. One feature of this embodiment is that it provides for efficient digital circuit verification. This Abstract is provided for the sole purpose of complying with the Abstract requirement rules that allow a reader to quickly ascertain the subject matter of the disclosure contained herein. This Abstract is submitted with the explicit understanding that it will not be used to interpret or to limit the scope or the meaning of the claims.

8326592, Dec 4, 2012

Dec 20, 2008

12/340670

Kenneth L. McMillan - Berkeley CA, US

Cadence Design Systems, Inc. - San Jose CA

G06F 17/50

703 14, 716103, 716106, 716111

Disclosed is a method and system for providing an improved and flexible approach for handling models of hardware and software designs for verification activities. The semantics of the software and hardware are mapped to allow correct interfacing between the hardware and software models. This allows designers to more efficiently and accurately perform hardware/software co-verification.