Sciweavers

ICCD
2000
IEEE

Equivalence Checking Combining a Structural SAT-Solver, BDDs, and Simulation

14 years 3 months ago
Equivalence Checking Combining a Structural SAT-Solver, BDDs, and Simulation
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 intertwined 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 efficie...
Viresh Paruthi, Andreas Kuehlmann
Added 31 Jul 2010
Updated 31 Jul 2010
Type Conference
Year 2000
Where ICCD
Authors Viresh Paruthi, Andreas Kuehlmann
Comments (0)