Sciweavers

Share
DAC
2007
ACM

On Resolution Proofs for Combinational Equivalence

11 years 24 days ago
On Resolution Proofs for Combinational Equivalence
Modern combinational equivalence checking (CEC) engines are complicated programs which are difficult to verify. In this paper we show how a modern CEC engine can be modified to produce a proof of equivalence when it proves a miter unsatisfiable. If the CEC engine formulates the problem as a single SAT instance (call this na?ive), one can use the resolution proof of unsatisfiability as a proof of equivalence. However, a modern CEC engine does not directly invoke a SAT solver for the whole miter, but instead uses a variety of techniques such as structural hashing, detection of intermediate functional equivalences, and circuit re-writing to first simplify the problem. We show that in spite of using these simplification techniques, a CEC engine can be modified to generate a single (extended) resolution proof for the whole miter just as in the na?ive case. The benefit of having a single proof is that the proof verification program remains extremely simple, and its correctness is much easie...
Satrajit Chatterjee, Alan Mishchenko, Robert K. Br
Added 12 Nov 2009
Updated 12 Nov 2009
Type Conference
Year 2007
Where DAC
Authors Satrajit Chatterjee, Alan Mishchenko, Robert K. Brayton, Andreas Kuehlmann
Comments (0)
books