Improving SAT-based Combinational Equivalence Checking through circuit preprocessing

This paper presents a new implication tool (Vimplic) which can be used to improve SAT-based combinational equivalence checking. This tool quickly builds the implication graph of the miter circuit and traverse through it inferring implications among its nodes assignments. This set of implications and the miter circuit netlist are converted to conjunctive normal form (CNF) and submitted to the SAT solver in order to prove equivalence between the two circuits of the miter. Using Vimplic we have been able to dramatically reduce the overall verification time of several circuits outperforming the state-of-the-art techniques for CEC such as Berkmin561, NiVER, and C-SAT.