Equivalence checking combining a structural SAT-solver, BDDs, and simulation

Abstract

This paper presents a verification technique for functional comparison of large combinational circuits using a novel combination of known approaches. The idea is based on a tight integration of a structural satisfiability (SAT) solver, BDD sweeping, and random simulation; all three working on a shared graph representation of the circuit. The BDD sweeping and SAT solver are applied in an inter-twined manner both controlled by resource limits that are successively increased during each iteration. In this cooperative setting the BDD sweeping incrementally reduces the search space for the SAT solver until the problem is solved or the resource limits are exhausted. This approach improves on previous work in several ways: The integral application of the SAT solver significantly enhances the capacity and efficiency of BDD sweeping and extends its suitability for miscomparing designs. Further, the random simulation algorithm works on the compressed circuit graph and thus runs more efficiently. Our experiments demonstrate that the outlined approach is effective for a large class of equivalence checking instances by automatically adapting to the difficulty of the problem.