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

Volume

5

fYear

2001

fDate

2001

Firstpage

121

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Circuits and Systems, 2001. ISCAS 2001. The 2001 IEEE International Symposium on

Conference_Location

Sydney, NSW

Print_ISBN

0-7803-6685-9

Type

conf

DOI

10.1109/ISCAS.2001.922000

Filename

922000