本文提出了一種新穎的基於值域等價電路最佳化技術，基於可滿足性問題的有界序向電路等效驗證，驗證使用可滿足性解法器求解兩個深度有限的序向電路功能等價的簡化方法。其關鍵的想法是在最佳化有界序向電路等效驗證中，同時保持到下一個狀態的輸出值域等價。與其展開兩個時序電路，我們首先使用值域等價電路技術盡量減小他們。這是因為之前的時段可以被看成是測試向量產生器，產生所有的輸入向量到下一個時段，而且僅限值域，也就是所有的輸出組合，會被看作是下個時段所需的資訊。使用已知的條件，也就是於k - 1個時段內功能等效，強化他們有界深度k的等效性檢查。給予兩個序向電路進行驗證，我們首先驗證第一個時段的功能等效。如果第一個時段是不等效的，這兩個電路為非等效。相反，如果他們的第一時段是等效的，我們通過使用根據值域等價電路的邏輯優化方法，簡化組成第一個時段的電路。接下來，我們使用這種簡化的電路，驅動這兩個電路的下一時段，然後再次驗證其功能等效。此過程重複進行，直到驗證出有時段是不等效的，或達到指定的有界深度。實驗結果根據IWLS 2005測試電路集，表明提出的簡化方法比起之前的方法可以節省更多的驗證時間與準確度。

This paper presents a novel simplification method based on the range-equivalent circuit
optimization technique for the SAT-based bounded sequential equivalence checking
(BSEC), which verifies the functional equivalence of two sequential circuits with a
bounded depth by using a SAT solver. The key idea is to optimize the circuits in BSEC
model while keeping the output to the next state range-equivalent. Instead of unrolling
the two sequential circuits, we first minimize them with range-equivalent circuit technique.
This is because the previous timeframes can be seen as a pattern generator that
feeds input patterns to the next timeframe and only the range, i.e., all the output combinations,
are required information for the next timeframes. Using the known condition that
two sequential circuits are functionally equivalent within k - 1 timeframes, we enhance
their equivalence checking with the bounded depth k. Given two sequential circuits to
be verified, we first verify the functional equivalence of their 1st timeframes. If their 1st
timeframes are non-equivalent, these two circuit are non-equivalent. Conversely, if their
1st timeframes are equivalent, we simplify the circuit consisting of their 1st timeframes
by using the conventional logic optimization methods followed by the range-equivalent
circuit technique. Next, we use this simplified circuit to drive the next timeframes of these
two circuits, and then verify their functional equivalence again. This process repeats until
the timeframes under verification are non-equivalent or a user-specified bounded depth
has been reached. The experimental results show that the proposed simplification method
can save more verification time and provide more accurate verification compared to the
previous enhancement method on the set of IWLS 2005 benchmarks.

1 Introduction
2 Preliminaries
2.1 SAT-based BSEC
2.2 Range-equivalent Circuit
3 An Overview
4 Enhanced SAT-Based BSEC
5 Experimental Results
6 Conclusion

[1] Berkeley Logic Synthesis and Verification Group, “ABC: A System for Sequential Synthesis and Verification," http://www.eecs.berkeley.edu/ alanmi/abc/.
[2] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures instead of BDDs," in Proc. Design Automation Conference,
1999, pp. 317-320.
[3] A. Biere, A. Cimatti, E. M. Clarke, O. Strichmanm and Y. Zhu, “Bounded Model Checking," Advances in Computers, vol. 58, 2003.
[4] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, “Symbolic Model Checking without BDDs," in Proc. Tools and Algorithms for the Construction and Analysis of Systems,
1999, pp. 193-207.
[5] D. Brand, “Verification of Large Synthesized Designs," in Proc. International Conference
on Computer-Aided Design, 1993, pp. 534-537.
[6] Lynn C. L. Chang, Charles H. P. Wen, and J. Bhadra, “Speeding up Bounded Sequential
Equivalence Checking with Cross-Timeframe State-Pair Constraints from
Data Learning," in Proc. International Test Conference, 2009, pp. 1-8.
[7] Y. C. Chen and C. Y.Wang, “An Implicit Approach to Minimizing Range-Equivalent
Circuits," IEEE Trans. Computer-Aided Design, vol. 27, pp. 1942-1955, Nov. 2008.
[8] Y. C. Chen and C. Y. Wang, “Fast Detection of Node Mergers Using Logic Im-
18
plications," in Proc. International Conference on Computer-Aided Design, 2009,
pp. 785-788.
[9] Y. C. Chen and C. Y. Wang, “Node Addition and Removal in the Presence of Don’t
Cares," in Proc. Design Automation Conference, 2010, pp. 505-510.
[10] Y. C. Chen and C. Y. Wang, “Fast Node Merging with Don’t Cares Using
Logic Implications," IEEE Trans. Computer-Aided Design, vol. 29, pp. 1827-1832,
Nov. 2010.
[11] Y. C. Chen and C. Y. Wang, “Logic Restructuring Using Node Addition and Removal,"
IEEE Trans. Computer-Aided Design, vol. 31, pp. 260-270, Feb. 2012.
[12] E. I. Goldberg, M. R. Prasad, and R. K. Brayton, “Using SAT for Combinational
Equivalence Checking," in Proc. Design, Automation & Test in Europe, 2001,
pp. 114-121.
[13] S. Y. Huang, K. T. Cheng, K. C. Chen, C. Y. Huang, and F. Brewer, “AQUILA: An
Equivalence Checking System for Large Sequential Designs," IEEE Trans. Computers,
vol. 49, pp. 443-464, May 2000.
[14] A. Mishchenko, S. Chatterjee, and R. Brayton, “DAG-Aware AIG Rewriting: A
Fresh Look at Combinational Logic Synthesis," in Proc. Design Automation Conference,
2006, pp. 532-536.
[15] J. Moondanos, C. H. Seger, Z. Hanna, and D. Kaiss, “CLEVER: Divide and Conquer
Combinational Logic Equivalence VERification with False Negative Elimination, in
Proc. International on Conference Computer Aided Verification, 2001, pp. 131-143.
[16] S. Reda and A. Salem, “Combinational Equivalence Checking Using Boolean Satisfiability
and Binary Decision Diagrams, in Proc. Design, Automation & Test in
Europe, 2001, pp. 122-126.
19
[17] G. S. Tseitin, “On the Complexity of Derivation in Propositional Calculus," in Studies
in Constr. Math. and Math. Logic, 1968. pp. 115-125.
[18] A. Veneris, A. Smith, and M. S. Abadir, “Logic Verification based on Diagnosis
Technique," in Proc. Asia South Pacific Design Automation Conference, 2003,
pp. 538-543.
[19] S. C. Wu, C. Y. Wang, and Y. C. Chen, “Novel Probabilistic Combinational Equivalence
Checking," IEEE Trans. Very Large Scale Integration Systems, vol. 16, pp.
365-375, April 2008.
[20] W. Wu and M. S. Hsiao, “Mining Global Constraints with Domain Knowledge
for Improving Bounded Sequential Equivalence Checking," IEEE Trans. Computer-
Aided Design, vol. 27, pp. 197-201, Jan. 2006.
[21] http://iwls.org/iwls2005/benchmarks.html
[22] http://minisat.se/