Title :
Least fixpoint approximations for reachability analysis
Author :
In-Ho Moon ; Kakula, J. ; Shiple, T. ; Somenzi, F.
Author_Institution :
Dept. of Electr. & Comput. Eng., Colorado Univ., Boulder, CO, USA
Abstract :
The knowledge of the reachable states of a sequential circuit can dramatically speed up optimization and model checking. However, since exact reachability analysis may be intractable, approximate techniques are often preferable. H. Cho et al. (1996) presented the machine-by-machine (MBM) and frame-by-frame (FBF) methods to perform approximate finite state machine (FSM) traversal. FBF produces tighter upper bounds than MBM; however, it usually takes much more time and it may have convergence problems. In this paper, we show that there exists a class of methods-least fixpoint approximations-that compute the same results as RFBF ("reached FBF", one of the FBF methods). We show that one member of this class, which we call "least fixpoint MBM" (LMBM), is as efficient as MBM, but provably more accurate. Therefore, the trade-off that existed between MBM and RFBF has been eliminated. LMBM can compute RFBF-quality approximations for all the large ISCAS-89 benchmark circuits in a total of less than 9000 seconds.
Keywords :
approximation theory; circuit analysis computing; circuit optimisation; convergence of numerical methods; finite state machines; reachability analysis; sequential circuits; 9000 s; ISCAS-89 benchmark circuits; LMBM; RFBF; accuracy; approximate finite state machine traversal; convergence; efficiency; frame-by-frame method; least fixpoint MBM; least fixpoint approximations; machine-by-machine method; model checking; optimization; reachability analysis; reached FBF; sequential circuit reachable states; upper bounds; Benchmark testing; Circuit analysis computing; Circuit testing; Convergence; Moon; Reachability analysis; Sequential analysis; Sequential circuits; State-space methods; Upper bound;
Conference_Titel :
Computer-Aided Design, 1999. Digest of Technical Papers. 1999 IEEE/ACM International Conference on
Conference_Location :
San Jose, CA, USA
Print_ISBN :
0-7803-5832-5
DOI :
10.1109/ICCAD.1999.810618