Partitioned ROBDDs-a compact, canonical and efficiently manipulable representation for Boolean functions
- 23 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
We present a new representation for Boolean functions called Partitioned ROBDDs. In this representation we divide the Boolean space into 'k' partitions and represent a function over each partition as a separate ROBDD. We show that partitioned-ROBDDs are canonical and can be efficiently manipulated. Further they can be exponentially more compact than monolithic ROBDDs and even free BDDs. Moreover, at any given time, only one partition needs to be manipulated which further increases the space efficiency. In addition to showing the utility of partitioned-ROBDDs on special classes of functions, we provide automatic techniques for their construction. We show that for large circuits our techniques are more efficient in space as well as time over monolithic ROBDDs. Using these techniques, some complex industrial circuits could be verified for the first time.Keywords
This publication has 21 references indexed in Scilit:
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- Multilevel logic synthesis based on functional decision diagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Dynamic variable ordering for ordered binary decision diagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Advanced verification techniques based on learningPublished by Association for Computing Machinery (ACM) ,1995
- Efficient Boolean manipulation with OBDD's can be extended to FBDD'sIEEE Transactions on Computers, 1994
- Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagramsPublished by Association for Computing Machinery (ACM) ,1994
- Probabilistic verification of Boolean functionsFormal Methods in System Design, 1992
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Equivalence of free boolean graphs can be decided probabilistically in polynomial timeInformation Processing Letters, 1980
- The complexity of equivalence and containment for free single variable program schemesPublished by Springer Nature ,1978