SAT-Based Equivalence Checking Based on Circuit Partitioning and Special Approaches for Conflict Clause Reuse

This paper presents a new SAT-based CEC methodology for the verification of circuits with structural dependence. This methodology is based on circuit partitioning and special approaches for conflict clauses reuse, reducing highly the CEC problem complexity. Using this methodology it is possible to improve the overall verification time of similar and dissimilar circuits. For instance, for similar multiplier circuits it was possible to check equivalence up to 37 times 37 bit without any circuit topological information in nearly 40 minutes. For dissimilar circuits, the proposed methodology is able to check equivalence up to 24 times 24 bit in one hour overcoming the BDD-based approaches that using cutpoints cannot check beyond a 12 times 12 bit multiplier with reasonable time limit.