SAT-based unbounded symbolic model checking

This paper describes a SAT-based unbounded symbolic model checking algorithm. BDDs have-been widely used for symbolic model checking, but the approach suffers from memory overflow. The SAT procedure was exploited to overcome the problem, but it verified only the states reachable through a bounded number of transitions. The proposed algorithm deals with unbounded symbolic model checking. The conjunctive normal form is used to represent sets of states and the transition relation, and a SAT procedure is modified to compute the existential quantification required in obtaining a pre-image. Some optimization techniques are exploited, and the depth first search method is used for efficient safety-property checking. Experimental results show the proposed algorithm can check more circuits than BDD-based symbolic model checking tools.