loading...
Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets
Yokohama January 23-January 26
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASPDAC.2007.3581102007 Asia and South Pacific Design Au ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
S. Disch, Inst. of Comput. Sci., Albert-Ludwigs-Univ. Freiburg
C. Schollm, Inst. of Comput. Sci., Albert-Ludwigs-Univ. Freiburg
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.
Index Terms:
shared circuit structures, combinational equivalence checking, incremental SAT techniques, bounded model checking
Citation:
S. Disch, C. Schollm, "Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets," asp-dac, pp.938-943, 2007 Asia and South Pacific Design Automation Conference, 2007
Usage of this product signifies your acceptance of the Terms of Use.