Patent ID: 7661082

Claim:
A computer-implemented method of verifying a property in a digital design description the method comprising: (a) deriving an abstraction of the digital design description; (b) determining a counterexample by an approximate reachable state computation using a computer, the approximate reachable state computation relying on the abstraction, a property, and a search depth for the approximate reachable state computation; (c) justifying the counterexample with a minimum justification; (d) determining a justification frontier from a result of justifying the counterexample, wherein the justification frontier comprises a set of boundary variables and boundary variable assignments of the counterexample; (e) updating the abstraction from a subset of the justification frontier; and (f) producing a verification result for the digital design description, from the determining of the counterexample by the approximate reachable state computation or the determining of justification frontier.