| |
|
|
Efficient Application of SAT and BDDs for Equivalence CheckingAndreas Kuehlmann AbstractEquivalence checking, namely the test of whether two combinational circuits implement the same Boolean function is a classical application of a SAT procedure. SAT and APTG algorithms have been extensively researched in the AI and CAD community which resulted in a number of efficient techniques to deal with large scale problems. Because of their generally inferior performance compared to BDD based techniques, the various attempts to adopt plain SAT procedures to equivalence checking had only limited success. However, BDD and SAT techniques have complementary strengths for different classes of problems; a hybrid algorithm that dynamically exploits their individual strength is highly desirable.In this talk, we present an equivalence checking technique that employs BDD sweeping and SAT search in a common setting. First, we will reiterate the basics of the BDD sweeping algorithm followed by implementations details of a new network based SAT procedure. We will then discuss how both techniques are combined in an intertwined manner for maximum combined performance. Experimental results and a discussion of future work will conclude the talk.
|
| Contact |
| ©2002-2018 U.C. Regents |