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
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;
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 1997. ICCD '97. Proceedings., 1997 IEEE International Conference on
Conference_Location :
Austin, TX
Print_ISBN :
0-8186-8206-X
DOI :
10.1109/ICCD.1997.628891