Title :
On the use of don´t cares during symbolic reachability analysis
Author :
Reda, S. ; Wahba, A. ; Salem, A. ; Borrione, D. ; Ghonaimy, M.
Author_Institution :
Fac. of Eng., Ain Shams Univ., Cairo, Egypt
Abstract :
We present a new symbolic algorithm for reachability analysis in sequential circuits. Using don´t cares from the computed reachable states, we introduce flexibility in choosing the transition relation, which can be used to minimize its Binary Decision Diagram (BDD). This can reduce the time-consuming image computation step. The technique is implemented and integrated in our equivalence checking system M-CHECK and its efficiency is shown on the ISCAS-89 benchmark circuits
Keywords :
binary decision diagrams; circuit analysis computing; formal verification; logic CAD; reachability analysis; sequential circuits; symbol manipulation; BDD minimisation; M-CHECK; binary decision diagrams; don´t cares; equivalence checking system; sequential circuits; symbolic algorithm; symbolic reachability analysis; transition relation; Automata; Binary decision diagrams; Boolean functions; Circuit synthesis; Computer graphics; Data structures; Image storage; Reachability analysis; Sequential circuits; Very large scale integration;
Conference_Titel :
Circuits and Systems, 2001. ISCAS 2001. The 2001 IEEE International Symposium on
Conference_Location :
Sydney, NSW
Print_ISBN :
0-7803-6685-9
DOI :
10.1109/ISCAS.2001.922000
