Abstract
We propose a BDD based representation for Boolean functions, which extends conjunctive/disjunctive decompositions. The model introduced (Meta-BDD) can be considered as a symbolic representation of k-Layer automata describing Boolean functions. A layer is the set of BDD nodes labeled by a given variable, and its characteristic function is represented using BDDs. Meta-BDDs are implemented upon a standard BDD library and they support layered (decomposed) processing of Boolean operations used in formal verification problems. Besides targeting reduced BDD size, the theoretical advantage of this form over other decompositions is being closed under complementation, which makes Meta-BDDs applicable to a broader range of problems.
Chapter PDF
Similar content being viewed by others
Keywords
- Boolean Function
- Binary Decision Diagram
- Reachability Analysis
- Deterministic Finite Automaton
- Order Binary Decision Diagram
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
R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
R. E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.
R. Rudell. Dynamic Variable Ordering for Ordered Binary Decision Diagrams. In Proc. IEEE/ACM ICCAD’93, pages 42–47, San Jose, California, November 1993.
J. Jain, J. Bitner, J. A. Abraham, and D. S. Fussel. Functional Partitioning for Verification and Related Problems. In Brown/MIT VLSI Conference, pages 210–226, March 1992.
K. L. McMillan. A conjunctively decomposed boolean representation for symbolic model checking. Proc. CAV’96, Lecture Notes in Computer Science 1102, Springer Verlag, pages 13–25, August 1996.
G.J. Holzmann and A. Puri. A minimized automaton representation of reachable states. Software Tools for Technology Transfer,Springer Verlag, 3(1), 1999.
O. Coudert, C. Berthet, and J. C. Madre. Verification of Sequential Machines Based on Symbolic Execution. In Lecture Notes in Computer Science 407, Springer Verlag, pages 365–373, Berlin, Germany, 1989.
H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit Enumeration of Finite State Machines Using BDDs. In Proc. IEEE IC-CAD’90, pages 130–133, San Jose, California, November 1990.
O. Coudert and J. C. Madre. A Unified Framework for the Formal Verification of Sequential Circuits. In Proc. IEEE ICCAD’90, pages 126–129, San Jose, California, November 1990.
R.K. Brayton R.K. Ranjan, J.V. Sanghavi and A. Sangiovanni-Vincentelli. High performance bdd package based on exploiting memory hierarchy. Proc. ACM/IEEE DAC’96, pages 635–640, June 1996.
F. Somenzi. CUDD: CU Decision Diagram Package-Release 2.3.0. Technical report, Dept. of Electrical and Computer Engineering, University of Colorado, Boulder, Colorado, October 1998.
MCNC Private Communication.
K. Ravi and F. Somenzi. Hints to Accelerate Symbolic Traversal. In Correct Hardware Design and Verification Methods (CHARME’99), pages 250–264, Berlin, September 1999. Springer-Verlag. LNCS 1703.
R. K. Ranjan, A. Aziz, R. K. Brayton, B. Plessier, and C. Pixley. Efficient BDD Algorithms for FSM Synthesis and Verification. In IWLS’95: IEEE International Workshop on Logic Synthesis, Lake Tahoe, California, May 1995.
A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new Symbolic Model Verifyer. In Proc. CAV’99, Lecture Notes in Computer Science 1633, Springer Verlag, pages 495–499, July 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cabodi, G. (2001). Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_11
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive