Iterative abstraction using SAT-based BMC with proof analysis
AssigneeNEC Laboratories America, Inc.
InventorsAarti Gupta, Malay Ganai, Zijiang Yang, Pranav Ashar
Life of this patent
Estimating the term…
Abstract
A method of obtaining a resolution-based proof of unsatisfiability using a SAT procedure for a hybrid Boolean constraint problem comprising representing constraints as a combination of clauses and interconnected gates. The proof is obtained as a combination of clauses, circuit gates and gate connectivity constraints sufficient for unsatisfiability.
Claims7
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.
A computer implemented method for verification of a given correctness property on a sequential circuit design, comprising the steps:
- (a) if the property is violated at depth k using a satisfiability-based bounded model checking, terminating the verification,
- (b) if the property is proved correct at depth k using a satisfiability-based bounded model checking, deriving an abstract model An from a proof of unsatisfiability generated by the satisfiability solver,
- (c) increasing the depth of unrolling k in bounded model checking,
- (d) repeating steps (a-c), constituting an inner loop comprising the bounded model checking iterations, until either there is no change in the size of the derived abstract model as the depth of unrolling k is increased, or some limit kmax on k is reached,
- (e) repeating steps (a-d) by using bounded model checking on the derived abstract model An to derive a new abstract model A+1, these steps constituting an outer loop comprising the abstraction iterations, until either there is no change in the size of the derived abstract model or some limit on number of abstraction iterations is reached,
- (f) checking the given correctness property on the derived abstract model, and if the derived abstract model is proved correct, deeming the circuit design to be correct;
- otherwise, deeming the verification to be inconclusive.
Dependencies are inferred from the claim text.