Report Number: CS-TR-95-1561
Institution: Stanford University, Department of Computer Science
Title: Techniques for Efficient Formal Verification Using Binary
Decision Diagrams
Author: Hu, Alan John
Date: December 1995
Abstract: The appeal of automatic formal verification is that it's
automatic -- minimal human labor and expertise should be
needed to get useful results and counterexamples. BDD(binary
decision diagram)-based approaches have promised to allow
automatic verification of complex, real systems. For large
classes of problems, however, (including many distributed
protocols, multiprocessor systems, and network architectures)
this promise has yet to be fulfilled. Indeed, the few
successes have required extensive time and effort from
sophisticated researchers in the field. This thesis
identifies several common obstacles to BDD-based automatic
formal verification and proposes techniques to overcome them
by avoiding building certain problematic BDDs needed in the
standard approaches and by exploiting automatically generated
and user-supplied don't-care information. Several examples
illustrate the effectiveness of the new techniques in
enlarging the envelope of problems that can routinely be
verified automatically.
http://i.stanford.edu/pub/cstr/reports/cs/tr/95/1561/CS-TR-95-1561.pdf