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.
