Patent ID: 7742907

Claim:
A computer implemented method for verification of a given correctness property on a sequential circuit design by using a satisfiability-based check for bounded model checking, comprising: (a) if the given correctness property is proved correct at a depth k, marking only flip-flops and external constraint nodes in the circuit design, based on whether their constraints appear in an unsatisfiable core generated from a proof of unsatisfiability by a satisfiability solver; otherwise, terminating verification, (b) deriving an abstract model consisting of combinational fanin cones of the marked flip-flops and external constraint nodes, (c) checking the given correctness property on the derived abstract model, and if the derived abstract model is proved correct, terminating the verification and deeming the circuit design to be correct. otherwise, increasing the depth of unrolling k and repeating steps (a)-(c) until either the given correctness property is violated at some depth or the circuit design is determined to be correct.