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.