Using Logic Synthesis and Circuit Reasoning for Equivalence Checking

Abstract:

Article Preview

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.

Info:

Periodical:

Advanced Materials Research (Volumes 201-203)

Edited by:

Daoguo Yang, Tianlong Gu, Huaiying Zhou, Jianmin Zeng and Zhengyi Jiang

Pages:

836-840

DOI:

10.4028/www.scientific.net/AMR.201-203.836

Citation:

Q. R. Fan et al., "Using Logic Synthesis and Circuit Reasoning for Equivalence Checking", Advanced Materials Research, Vols. 201-203, pp. 836-840, 2011

Online since:

February 2011

Export:

Price:

$35.00

In order to see related information, you need to Login.

In order to see related information, you need to Login.