Abstract
Many researchers have reported that using Boolean decision diagrams (BDDs) greatly increases the size of hardware designs that can be formally verified automatically. Our own experience with automatic verification of high-level aspects of hardware design, such as protocols for cache coherence and communications, contradicts previous results; in fact, BDDs have been substantially inferior to brute-force algorithms that store states explicitly in a table.
We believe that new techniques are needed to realize the potential advantages of BDD-based verification at the protocol level. Here, we isolate several common causes of BDD-size blowup and show how these problems can be alleviated by a new verification approach based on partially evaluating the invariant being checked into an implicit conjunction of small BDDs. We describe the new method and give several examples of its application.
This research was supported by the Defense Advanced Research Projects Agency (contract number N00014-87-K-0828) and by a gift from Mitsubishi Electronics. The first author was supported by an ONR Graduate Fellowship. Most of this work was done using equipment generously donated by Sun Microsystems.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S. Bose and A. Fisher, “Automatic Verification of Synchronous Circuits Using Symbolic Logic Simulation and Temporal Logic,” IMEC-IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, Luc J.M. Claesen, ed., North Holland, 1989.
Karl S. Brace, Richard L. Rudell, and Randal E. Bryant, “Efficient Implementation of a BDD Package,” 27th ACM/IEEE Design Automation Conference, 1990, pp. 40–45.
Randal E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers, Vol. C-35, No. 8 (August 1986), pp. 677–691.
J.R. Burch, E.M. Clarke, and D.E. Long, “Symbolic Model Checking with Partitioned Transition Relations,” VLSI '91: Proceedings of the IFIP TC10/WG 10.5 International Conference on Very Large Scale Integration, Edinburgh, Great Britain, 1991.
J.R. Burch, E.M. Clarke, K.L. McMillan, and David L. Dill, “Sequential Circuit Verification Using Symbolic Model Checking,” 27th ACM/IEEE Design Automation Conference, 1990, pp. 46–51.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, “Symbolic Model Checking: 1020 States and Beyond,” Proceedings of the Conference on Logic in Computer Science, 1990, pp. 428–439.
Hyunwoo Cho, Gary Hachtel, Seh-Woong Jeong, Bernard Plessier, Eric Schwarz, and Fabio Somenzi, “ATPG Aspects of FSM Verification,” IEEE International Conference on Computer-Aided Design, 1990, pp. 134–137.
Olivier Coudert, Christian Berthet, and Jean Christophe Madre, “Verification of Synchronous Sequential Machines Based on Symbolic Execution,” Automatic Verification Methods for Finite State Systems, J. Sifakis, ed., Lecture Notes in Computer Science Vol. 407, Springer-Verlag, 1989.
Olivier Coudert, Christian Berthet, and Jean Christophe Madre, “Verification of Sequential Machines Using Boolean Functional Vectors,” IMEC-IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, Luc J.M. Claesen, ed., North Holland, 1989.
David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang, “Protocol Verification as a Hardware Design Aid,” IEEE International Conference on Computer Design, October 1992.
Thomas Filkorn, “Functional Extension of Symbolic Model Checking,” Computer-Aided Verification: Third International Workshop, July 1–4, 1991, K.G. Larsen and A. Skou, eds., Lecture Notes in Computer Science Vol. 575, Springer-Verlag, published 1992.
Alan J. Hu and David L. Dill, “Reducing BDD Size by Exploiting Functional Dependencies,” 30th ACM/IEEE Design Automation Conference, 1993, to appear.
Alan J. Hu, David L. Dill, Andreas J. Drexler, and C. Han Yang, “Higher-Level Specification and Verification with BDDs,” Computer-Aided Verification: Fourth International Workshop, July 1992, to be reprinted in Springer-Verlag's LNCS Series.
S.-W. Jeong, B. Plessier, G.D. Hachtel, and F. Somenzi, “Variable Ordering for FSM Traversal,” Proceedings of the International Workshop on Logic Synthesis, MCNC, Research Triangle Park, NC, May 1991.
Timothy Y. K. Kam and Robert K. Brayton, “Multi-Valued Decision Diagrams,” UCB/ERL M90/125, December 1990.
Yung-Te Lai and Sarma Sastry, “Edge-Valued Binary Decision Diagrams for Multi-Level Hierarchical Verification,” 29th ACM/IEEE Design Automation Conference, 1992, pp. 608–613.
David E. Long, personal correspondence.
Arvind Srinivasan, Timothy Kam, Sharad Malik, and Robert K. Brayton, “Algorithms for Discrete Function Manipulation,” IEEE International Conference on Computer-Aided Design, 1990, pp. 92–95.
Herve J. Touati, Hamid Savoj, Bill Lin, Robert K. Brayton, and Alberto Sangiovanni-Vincentelli, “Implicit State Enumeration of Finite State Machines using BDD's” IEEE International Conference on Computer-Aided Design, 1990, pp. 130–133.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hu, A.J., Dill, D.L. (1993). Efficient verification with BDDs using implicitly conjoined invariants. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_2
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive