DocumentCode :
3163807
Title :
Equivalence checking using abstract BDDs
Author :
Jha, S. ; Lu, Y. ; Minea, M. ; Clarke, E.M.
Author_Institution :
Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
fYear :
1997
fDate :
12-15 Oct 1997
Firstpage :
332
Lastpage :
337
Abstract :
We introduce a new equivalence checking method based on abstract BDDs (aBDDs). The basic idea is the following: given an abstraction function, aBDDs reduce the size of BDDs by merging nodes that have the same abstract value. An aBDD has bounded size and can be constructed without constructing the original BDD. We show that this method of equivalence checking is always sound. It is complete for an important class of arithmetic circuits that includes integer multiplication. We also suggest heuristics for findings suitable abstraction functions based on the structure of the circuit. The efficiency of this technique is illustrated by experiments on ISCAS´85 benchmark circuits
Keywords :
abstract data types; computational complexity; formal verification; performance evaluation; ISCAS´85 benchmark circuits; abstract BDDs; abstraction function; abstraction functions; arithmetic circuits; bounded size; equivalence checking; heuristics; integer multiplication; Arithmetic; Binary decision diagrams; Bismuth; Boolean functions; Circuits; Computer science; Data structures; Formal verification; Merging; Table lookup;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 1997. ICCD '97. Proceedings., 1997 IEEE International Conference on
Conference_Location :
Austin, TX
ISSN :
1063-6404
Print_ISBN :
0-8186-8206-X
Type :
conf
DOI :
10.1109/ICCD.1997.628891
Filename :
628891
Link To Document :
بازگشت