Using Logic Synthesis and Circuit Reasoning for Equivalence Checking

Abstract:

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.

• Periodical: Advanced Materials Research (Volumes 201-203)
• Pages: 836-840
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.201-203.836
• Online since: February 2011
• Authors: Quan Run Fan, Feng Pan, Xin Dong Duan
• Keywords: And-Inverter Graph, Circuit Reasoning, Equivalence Checking, Logic Synthesis

References

[1] F. Lu and K. T. Cheng. Sequential Equivalence Checking Based on K-th Invariants and Circuits SAT solving. Proc. HLDVT Workshop'05, pp.45-52.

DOI: 10.1109/hldvt.2005.1568812

[2] A. Kuehlmann. Dynamic Transition Relation Simplication for Bounded Property Checking. Proc. ICCAD'04, pp.50-57.

[3] R. E. Bryant. Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C(35), 1986, pp.677-691.

DOI: 10.1109/tc.1986.1676819

[4] D. Brand. Verification of Large Synthesized Designs. Proc. ICCAD 93, pp.534-537.

[5] S. Cook. The Complexity of Theorem Proving Procedures. In ACM SIGACT Symposium on the Theory of Computing, (1971).

[6] A. Biere. AIGER (AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs). http: /fmv. jku. at/aiger.

[7] A. Kuehlman, M. K. Ganai, and V. Paruthi. Circuit-based Boolean Reasoning. Proc. DAC'01, pp.232-237.

[8] A. Kuehlman, V. Paruthi, F. Krohm, and M. K. Ganai. Robust Boolean Reasoning for Equivalence Checking and functional Property Verification. IEEE Trans. CAD, 21(12), 2002, pp.1377-1394.

DOI: 10.1109/tcad.2002.804386

[9] E. I. Goldberg, M. R. Prasad, and R. K. Brayton, Using SAT for Combinational Equivalence Checking. Proc. Conference on Design Automation and Test in Europe, 2001, pp.114-121.

DOI: 10.1109/date.2001.915010

[10] Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. Release 70930. http: /www. eecs. berkeley. edu/~alanmi/abc.

[11] F. Lu, L. Wang, K. Cheng, R. Huang. A Circuit SAT Solver with Signal Correlation Guided Learning. Proc. European Design and Test Conference, March (2003).

DOI: 10.1109/date.2003.1253719

[12] F. Lu, L. Wang, K. Cheng, J. Moondanos and Z. Hanna. A Signal Correlation Guided ATPG Solver And Its Applications for Solving Difficult Industrial Cases. Proc. Design Automation Conference, June (2003).

DOI: 10.1145/775832.775947

[13] J. N. Hooker. Solving the incremental satisfiability problem. Journal of Logic Programming, vol. 15, no. 1-2, 1993, pp.177-186.

DOI: 10.1016/0743-1066(93)90018-c

[14] Quartus II University Interface Program. www. altera. com/education/univ/research/unquip. html.

[15] N. Een and N. Sorensson. An Extensible Sat-solver. Theory and Applications of Satisfiability Testing, 6th International Conference, SAT2003.

[16] J. Pistorius, M. Hutton, A. Mishchenko, and R. Brayton. Benchmarking method and designs targeting logic synthesis for FPGAs. Proc. IWLS '07, pp.230-237.

[17] PicoSAT. http: /fmv. jku. at/picosat.