We describe the techniques we have used to search for bugs in the memory
subsystem of a next-generation Alpha microprocessor. Our approach is
based on two model checking methods that use satisfiability (SAT) solvers
rather than binary decision diagrams (BDDs).
We show that the first method, bounded model checking, can reduce the
verification runtime from days to minutes on real, deep, microprocessor
bugs when compared to a state-of-the-art BDD-based model checker. We also
present experimental results showing that the second method, a version of
symbolic trajectory evaluation that uses SAT-solvers instead of BDDs, can
find as deep bugs, with even shorter runtimes. The tradeoff is that we
have to spend more time writing specifications.
Finally, we present our experience with the two SAT-solvers that we have
used, and give guidelines for applying a combination of bounded model
checking and symbolic trajectory evaluation to industrial strength
verification.
The bugs we have found are significantly more complex than those
previously found with methods based on SAT-solvers.
