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...

• Type: Conference
• Year: 2007
• Where: DAC
• Authors: Satrajit Chatterjee, Alan Mishchenko, Robert K. Brayton, Andreas Kuehlmann
• Keywords: DAC 2007, Design Automation, Modern Cec Engine, Modern Combinational Equivalence, Proof Verification Program