Reachability analysis using partitioned-ROBDDs
- 1 January 1997
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 1102 (10923152) , 388-393
- https://doi.org/10.1109/iccad.1997.643565
Abstract
We address the problem of finite state machine (FSM) traversal, a key step in most sequential verification and synthesis algorithms. We propose the use of partitioned ROBDDs to reduce the memory explosion problem associated with symbolic state space exploration techniques. In our technique, the reachable state set is represented as a partitioned ROBDD (A. Narayan et al., 1996). Different partitions of the Boolean space are allowed to have different variable orderings and only one partition needs to be in memory at any given time. We show the effectiveness of our approach on a set of ISCAS89 benchmark circuits. Our techniques result in a significant reduction in total memory utilization. For a given memory limit, partitioned ROBDD based method can complete traversal for many circuits for which monolithic ROBDDs fail. For circuits where both partitioned ROBDDs as well as monolithic ROBDDs cannot complete traversal, partitioned ROBDDs can reach a significantly larger set of states.Keywords
This publication has 20 references indexed in Scilit:
- Improved reachability analysis of large finite state machinesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Implicit state enumeration of finite state machines using BDD'sPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- High-density reachability analysisPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Disjunctive Partitioning And Partial Iterative Squaring: An Effective Approach For Symbolic Traversal Of Large CircuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1997
- Indexed BDDs: algorithmic advances in techniques to represent and verify Boolean functionsIEEE Transactions on Computers, 1997
- On the descriptive and algorithmic power of parity ordered binary decision diagramsPublished by Springer Nature ,1997
- Graph driven BDDs — a new data structure for Boolean functionsTheoretical Computer Science, 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
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986