SAT-based Verification without State Space Traversal

Per Bjesse and Koen Claessen

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


The area of symbolic model checking has been dominated by Binary Decision Diagrams (BDDs) for the past decade. Recently, the use of satisfiability (SAT) solvers has emerged as an interesting complement to BDDs. The resulting model checking methods are capable of coping with some of the systems that BDDs are unable to handle. The most challenging problem that has to be solved in order to adapt standard symbolic model checking to SAT-solvers is the boolean quantification necessary for traversing the state space. A simple way of extending the range of hard systems that SAT-based model checkers can handle, is therefore to reduce the necessary amount of traversal. In this paper, we investigate a BDD-based verification algorithm due to van Eijk, which is not based on state space traversal. The analysis computes information about the circuit that either is sufficient to verify a safety property directly, or that can be used to reduce the amount of traversal needed in conventional model checking methods. We convert van Eijk's algorithm to use a SAT-solver so that we can use it also for circuits that blow up when represented with BDDs. Furthermore, we make a sequence of improvements to the original algorithm, such as combining it with SAT-based induction. The result is a collection of substantially strengthened and complete methods for verifying safety properties of circuits without state space traversal.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Start Conference Manager
Conference Systems