Efficient SAT-based unbounded symbolic model checking

1. A computer-implemented method of solving a SAT-based quantifier elimination problem, said method comprising the following steps:

enumerating, as a result of a series of calls to a SAT solver, satisfying solutions for a given Boolean formula;

cofactoring the given Boolean formula with a satisfying minterm over the variables to be quantified, in order to capture one or more satisfying states enumerated by the SAT solver, and to additionally capture some satisfying states that cannot be captured by a cube and that have not yet been enumerated by the SAT solver;

representing, a suitably efficient representation of the captured states; and

generating, a computer-generated output of the suitably efficient representation.

2. The method of claim 1 , wherein the quantification includes a BDD-based quantification.

3. The method of claim 1 , wherein the captured set of satisfying states that have not yet been enumerated by the SAT solver is increasing.

4. The method of claim 1 , wherein the captured set of satisfying states that have not yet been enumerated by the SAT solver is increasing, and the satisfying minterm is heuristically chosen.

5. The method of claim 1 , wherein Boolean operations and state representations are represented by semi-canonical circuit representations.

6. The method of claim 1 wherein the enumeration step includes generating partial satisfying assignments through the use of a hybrid SAT solver.

7. A computer implemented method for computing backward reachable states iteratively, said method comprising the steps of:

a) unrolling a design, successively in a step-by-step manner;

b) calculating, a pre-image across multiple time frames in the unrolled design in each of the successive steps;

c) updating, a set of backward reachable states, starting from a given set of target states, in each of the successive steps; and

d) repeating, the steps a-c until a suitable termination criterion on the backward reachable states is obtained; and

e) generating, a computer-generated output of the suitably efficient representation;

wherein said calculating step further comprises the steps of:

enumerating, as a result of a series of calls to a SAT solver, satisfying solutions for a given Boolean formula;

cofactoring the given Boolean formula with a satisfying miniterm over the variables to be quantified, in order to capture one or more satisfying states enumerated by the SAT solver, and to additionally capture some satisfying states that cannot be captured by a cube and that have not been enumerated by the SAT solver; and

representing, a suitably efficient representation of the captured states.

8. The method of claim 7 , wherein the quantification includes a BDD-based quantification.

9. The method of claim 7 , wherein the captured set of satisfying states that have not yet been enumerated by the SAT solver is increasing.

10. The method of claim 7 , wherein the captured set of satisfying states that have not yet been enumerated by the SAT solver is increasing, and the satisfying minterm is heuristically chosen.

11. The method of claim 7 , wherein Boolean operations and state representations are represented by semi-canonical circuit representations.

12. The method of claim 7 , wherein the enumeration step includes generating partial satisfying assignments through the use of a hybrid SAT solver.

13. The method according to claim 7 wherein the pre-image calculated is an approximate pre-image.

14. The method according to claim 7 further comprising the step of:

setting a threshold on the number of SAT enumerations.

15. The method of claim 7 , wherein said pre-image computation step includes additional constraints to exclude previously-reached states.

16. The method of claim 7 wherein said state-set is represented by a circuit-graph representation.

17. The method according to claim 7 further comprising the step of:

additionally using an external invariant such that the termination condition is achieved in a smaller number of steps.

18. A computer implemented method for computing backward reachable states iteratively, said method comprising the steps of:

a) calculating, a pre-image across a single time frame of a design in each of the successive steps; said calculating step including:

enumerating, as a result of a series of calls to a SAT solver, satisfying solutions for a given Boolean formula;

cofactoring the given Boolean formula with a satisfying minterm over the variables to be quantified, in order to capture one or more satisfying states enumerated by the SAT solver, and to additionally capture some satisfying states that cannot be captured by a cube and that have not yet been enumerated by the SAT solver; and

representing, a suitably efficient representation of the captured states;

b) updating, a set of backward reachable states, starting from a given set of target states, in each of the successive steps; and

c) repeating, the steps a-b until a suitable termination criterion on the backward reachable states is obtained; and

d) generating, a computer-generated output of the captured states.

19. The method of claim 18 , wherein the quantification includes a BDD-based quantification.

20. The method of claim 18 , wherein the captured set of satisfying states that have not yet been enumerated by the SAT solver is increasing.

21. The method of claim 18 , wherein the captured set of satisfying states that have not yet been enumerated by the SAT solver is increasing, and the satisfying minterm is heuristically chosen.

22. The method of claim 18 , wherein Boolean operations and state representations are represented by semi-canonical circuit representations.

23. The method of claim 18 wherein the enumeration step includes generating partial satisfying assignments through the use of a hybrid SAT solver.

24. The method according to claim 18 wherein the pre-image calculated is an approximate pre-image.

25. The method according to claim 18 further comprising the step of: setting a threshold on the number of SAT enumerations.

26. The method of claim 18 , wherein said pre-image computation step includes additional constraints to exclude previously-reached states.

27. The method of claim 18 wherein said state-set is represented by a circuit-graph representation.

28. The method according to claim 18 further comprising the step of:

additional use of an external invariant such that the termination condition is achieved in a smaller steps.