DocumentCode :
2547172
Title :
Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets
Author :
Disch, Stefan ; Scholl, Christoph
Author_Institution :
Inst. of Comput. Sci., Albert-Ludwigs-Univ. Freiburg
fYear :
2007
fDate :
23-26 Jan. 2007
Firstpage :
938
Lastpage :
943
Abstract :
Combinational equivalence checking is an essential task in circuit design. In this paper we focus on SAT based equivalence checking making use of incremental SAT techniques which are well known from their application in bounded model checking. Based on an analysis of shared circuit structures we present heuristics which try to maximize the benefit from incremental SAT solving in this application by looking for good orders in which the equivalence of different circuit outputs is checked. Moreover, we present a reset strategy for situations where the benefit from the incremental SAT approach seems to decrease. Experimental results demonstrate that our novel method outperforms traditional methods significantly.
Keywords :
combinational circuits; computability; equivalence classes; bounded model checking; combinational equivalence checking; incremental SAT techniques; shared circuit structures; Application software; Boolean functions; Circuit analysis; Circuit synthesis; Computer science; Context modeling; Logic circuits; State-space methods; Tin; Very large scale integration;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Design Automation Conference, 2007. ASP-DAC '07. Asia and South Pacific
Conference_Location :
Yokohama
Print_ISBN :
1-4244-0629-3
Electronic_ISBN :
1-4244-0630-7
Type :
conf
DOI :
10.1109/ASPDAC.2007.358110
Filename :
4196156
Link To Document :
بازگشت