Early quantification and partitioned transition relations
- 24 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Hardware systems are generally specified as a set of interacting finite state machines (FSMs). An important problem in formal verification using Binary Decision Diagrams (BDDs) is forming the transition relation of the product machine. This problem reduces to conjuncting (or multiplying) the BDDs representing the transition relations of the individual machines, and then existentially quantifying out the set of input and output variables. The resulting graph is called the product graph. Computing the set of reachable states of the product graph is the central verification problem. In this paper, we discuss two related problems. The early quantification problem is the problem of interleaving multiplication of a set of BDDs with the quantification of a set of variables so that the size of the largest BDD encountered is minimized. We show that an abstraction of this problem is NP-complete, and provide heuristic solutions for it. In some cases, the size of the BDD representing the transition relation of the product graph is too large. The partitioned transition relations problem deals with partially combining the BDD脝s and quantifying as many variables as possible, so that the time for computing the set of reachable states of the product graph is minimized. We offer heuristic solutions to this problem based on our algorithms for early quantification. The algorithms have been implemented and good experimental results have been achieved.Keywords
This publication has 10 references indexed in Scilit:
- Exploiting cofactoring for efficient FSM symbolic traversal based on the transition relationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Dynamic variable ordering for ordered binary decision diagramsPublished 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
- HSISPublished by Association for Computing Machinery (ACM) ,1994
- A fully implicit algorithm for exact state minimizationPublished by Association for Computing Machinery (ACM) ,1994
- Symbolic Model CheckingPublished by Springer Nature ,1993
- Representing circuits more efficiently in symbolic model checkingPublished by Association for Computing Machinery (ACM) ,1991
- Complexity of Finding Embeddings in a k-TreeSIAM Journal on Algebraic Discrete Methods, 1987
- Graph minors. II. Algorithmic aspects of tree-widthJournal of Algorithms, 1986
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986