Hybrid decision diagrams. Overcoming the limitations of MTBDDs and BMDs
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10636757,p. 159-163
- https://doi.org/10.1109/iccad.1995.480007
Abstract
Functions that map boolean vectors into the integers are important for the design and verification of arithmetic circuits. MTBDDs and BMDs have been proposed for representing this class of functions. We discuss the relationship between these methods and describe a generalization called hybrid decision diagrams which is often much more concise. We show how to implement arithmetic operations efficiently for hybrid decision diagrams. In practice, this is one of the main limitations of BMDs since performing arithmetic operations on functions expressed in this notation can be very expensive. In order to extend symbolic model checking algorithms to handle arithmetic properties, it is essential to be able to compute the BDD for the set of variable assignments that satisfy an arithmetic relation. In our paper, we give an efficient algorithm for this purpose. Moreover, we prove that for the class of linear expressions, the time complexity of our algorithm is linear in the number of variables.Keywords
This publication has 8 references indexed in Scilit:
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- Fast OFDD-based minimization of fixed polarity Reed-Muller expressionsIEEE Transactions on Computers, 1996
- Verification of arithmetic circuits with binary moment diagramsPublished by Association for Computing Machinery (ACM) ,1995
- Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagramsPublished by Association for Computing Machinery (ACM) ,1994
- Algebraic decision diagrams and their applicationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1993
- Spectral transforms for large boolean functions with applications to technology mappingPublished by Association for Computing Machinery (ACM) ,1993
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Application of Boolean algebra to switching circuit design and to error detectionTransactions of the I.R.E. Professional Group on Electronic Computers, 1954