Using Logic Synthesis and Circuit Reasoning for Equivalence Checking
Quanrun Fan, Feng Pan, Xin Duan · Advanced materials research · 2011
The existing SAT based algorithms combines two circuits into a miter, and then convert the miter into a CNF formula. After that, a SAT solver is invoked to check the satisfiability of the CNF formula. However, when a miter is converted into CNF formula, the structure information of the circuit is lost. Therefore,we are motivated to solve the problem of miter satisfiability using circuit reasoning. We use logic synthesis first to simplify the circuit, and then use a backtracking method to check the satisfiability of the miter. The preliminary experimental result sindicate that our approach is efficient.