The Community for Technology Leaders
Proceedings International Conference on Computer Design VLSI in Computers and Processors (1997)
Austin, TX
Oct. 12, 1997 to Oct. 15, 1997
ISSN: 1063-6404
ISBN: 0-8186-8206-X
pp: 332
S. Jha , Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
Y. Lu , Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
M. Minea , Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
E.M. Clarke , 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.
INDEX TERMS
performance evaluation; equivalence checking; abstract BDDs; abstraction function; bounded size; arithmetic circuits; integer multiplication; heuristics; abstraction functions; ISCAS'85 benchmark circuits
CITATION

M. Minea, E. Clarke, Y. Lu and S. Jha, "Equivalence checking using abstract BDDs," Proceedings International Conference on Computer Design VLSI in Computers and Processors(ICCD), Austin, TX, 1997, pp. 332.
doi:10.1109/ICCD.1997.628891
92 ms
(Ver 3.3 (11022016))