High-density reachability analysis
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10636757,p. 154-158
- https://doi.org/10.1109/iccad.1995.480006
Abstract
We address the problem of reachability analysis for large finite state systems. Symbolic techniques have revolutionized reachability analysis but still have limitations in traversing large systems. We present techniques to improve the symbolic breadth-first traversal and compute a lower bound on the reachable states. We identify the problem as one of density during traversal and our techniques seek to improve the same. Our results show a marked improvement on the existing breadth-first traversal methods.Keywords
This publication has 7 references indexed in Scilit:
- Protocol verification as a hardware design aidPublished 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
- Variable ordering and selection of FSM traversalPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- ATPG aspects of FSM verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Efficient implementation of a BDD packagePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Symbolic model checking for sequential circuit verificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986