Using Logic Synthesis and Circuit Reasoning for Equivalence Checking
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.
Daoguo Yang, Tianlong Gu, Huaiying Zhou, Jianmin Zeng and Zhengyi Jiang
Q. R. Fan et al., "Using Logic Synthesis and Circuit Reasoning for Equivalence Checking", Advanced Materials Research, Vols. 201-203, pp. 836-840, 2011