Title :
High-density reachability analysis
Author :
Ravi, K. ; Somenzi, F.
Author_Institution :
Dept. of Electr. & Comput. Eng., Colorado Univ., Boulder, CO, USA
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 :
circuit analysis computing; finite state machines; reachability analysis; breadth-first traversal methods; high-density reachability analysis; large finite state systems; lower bound; symbolic breadth-first traversal; symbolic techniques; Automata; Binary decision diagrams; Boolean functions; Circuits; Data structures; Density measurement; Reachability analysis; Sampling methods; State-space methods; Upper bound;
Conference_Titel :
Computer-Aided Design, 1995. ICCAD-95. Digest of Technical Papers., 1995 IEEE/ACM International Conference on
Conference_Location :
San Jose, CA, USA
Print_ISBN :
0-8186-8200-0
DOI :
10.1109/ICCAD.1995.480006
