Binary Decision Diagrams (BDDs) have enabled formal
verification to tackle larger hardware designs than before. However
for many large design examples, even the most sophisticated
BDD-based verification methods cannot produce exact results because
of size blowup. However, required properties of a design rarely
rely on every implementation detail of the design, so
approximate verification algorithms may yield meaningful
results while handling larger designs.
Approximate reachability techniques trade off accuracy for
the capacity to deal with bigger designs. In this paper, we
extend the idea of approximations using overlapping projections to
symbolic backward reachability. This is combined with a previous
method of computing overapproximate forward reachable state sets
using overlapping projections. The algorithm computes a superset
of the set of states that lie on a path from the initial state to
a state that violates a specified invariant property. If this set
is empty, there is no possibility of violating the invariant. If
this set is non-empty, it may be possible to prove the existence
of such a path by searching for a counter-example. A simple
heuristic is given, which seems to work well in practice, for
generating a counter-example path from this approximation. We
evaluate these new algorithms by applying them to several control
modules from the I/O unit in the Stanford FLASH Multiprocessor.