這個研究提出一個基於值域等價電路技術(range-equivalent circuit technique)的
方法來加速以可滿足性問題為基底(SAT-based)的有界序向電路的等價驗
證(Bounded Sequential Equivalence Checking)。給定兩個需要驗證的序向電路，
我們不直接展開這兩個序向電路產生的銜接電路，在展開一個銜接電路的時間框
架以前，我們反覆的利用值域等價電路技術來縮小銜接電路。這是因為前面的時
間框架可以被視為一個樣式的產生器(pattern generator)，並且這個樣式的產生器
只需要傳遞前面時間框架的值域給下一個時間框架。實驗結果顯示，當有界序向
電路達到同樣深度時，跟之前的研究比較起來，我們提出的方法在IWLS2005的測
試電路上可以節省高達91百分比的驗證時間。

This paper presents a method based on
range-equivalent circuit technique for SAT-based
bounded sequential equivalence checking.
Given two sequential circuits to
be verified, instead of straightforward unrolling the miter of two
sequential circuits, we iteratively minimize the miter with a range-equivalent
circuit technique before adding a new timeframe.
This is because the previous timeframes can be
seen as a pattern generator that feeds input patterns to the next
timeframe and only the ranges of previous timeframes are required information for the next
timeframe. Experimental results show that the proposed method saved up to 91 percent of
verification time for reaching the same bounded depth compared
with previous work on a set of IWLS2005 benchmarks.

[1] J. Baumgartner and H. Mony, “Maximal Input Reduction of Sequential
Netlists via Synergistic Reparameterization and Localization Strategies,”
in Proc. Advanced Research Working Conference on Correct Hardware
Design and Verification Methods, 2005, pp. 222-237.
[2] Berkeley Logic Synthesis and Verification Group, “ABC:
A System for Sequential Synthesis and Verification,”
http://www.eecs.berkeley.edu/ alanmi/abc/.
[3] A. Biere, et al. “Symbolic Model Checking Using SAT Procedures
instead of BDDs,” in Proc. DAC, 1999, pp. 317-320.
[4] A. Biere, et al. “Bounded Model Checking,” Advances in Computers,
vol. 58, 2003, pp. 117-148.
[5] A. Biere, et al. “Symbolic Model Checking without BDDs,” in
Proc. Tools and Algorithms for the Construction and Analysis of
Systems, 1999, pp. 193-207.
[6] D. Brand, “Verification of Large Synthesized Designs,” in Proc. ICCAD,
1993, pp. 534-537.
[7] Lynn C. L. Chang, et al. “Speeding up Bounded Sequential Equivalence
Checking with Cross-Timeframe State-Pair Constraints from Data
Learning,” in Proc. ITC, 2009, pp. 1-8.
[8] P. Chauhan, et al., “A SAT-Based Algorithm for Reparameterization in
Symbolic Simulation,” in Proc. DAC, 2004, pp. 524-529.
[9] Y. C. Chen and C. Y. Wang, “An Implicit Approach to Minimizing
Range-Equivalent Circuits,” IEEE TCAD, vol. 27, pp. 1942-1955,
Nov. 2008.
[10] Y. C. Chen and C. Y. Wang, “Node Addition and Removal in the
Presence of Don’t Cares,” in Proc. DAC, 2010, pp. 505-510.
[11] Y. C. Chen and C. Y. Wang, “Fast Node Merging with Don’t Cares Using
Logic Implications,” IEEE TCAD, vol. 29, pp. 1827-1832, Nov. 2010.
[12] Y. C. Chen and C. Y. Wang, “Logic Restructuring Using Node Addition
and Removal,” IEEE TCAD, vol. 31, pp. 260-270, Feb. 2012.
[13] N. Een and A. Mishchenko, “A Fast Reparameterization Procedure,” in
Proc. DIFTS, 2013, pp. 4-8.
[14] Niklas Een and Niklas Srensson, “MiniSat - A SAT Solver with Conflict-
Clause Minimization,” in Proc. SAT, 2005.
[15] E. I. Goldberg, et al. “Using SAT for Combinational Equivalence
Checking,” in Proc. DATE, 2001, pp. 114-121.
[16] S. Y. Huang, et al. “AQUILA: An Equivalence Checking System for
Large Sequential Designs,” IEEE TC, vol. 49, pp. 443-464, May 2000.
[17] A. Mishchenko, et al. “DAG-Aware AIG Rewriting: A Fresh Look at
Combinational Logic Synthesis,” in Proc. DAC, 2006, pp. 532-536.
[18] J. P. Marques-Silva and K.A. Sakallah, “GRASP - A New Search
Algorithm for Satisfiability,” IEEE TC, vol. 48, pp. 506-521, May 1999.
[19] J. Moondanos, et al. “CLEVER: Divide and Conquer Combinational
Logic Equivalence VERification with False Negative Elimination,” in
Proc. CAV, 2001, pp. 131-143.
[20] S. M. Plaza, et al., “Node Mergers in the Presence of Don’t Cares,” in
Proc. ASPDAC, 2007, pp. 414-419.
[21] M. W. Moskewicz, et al., “Chaff: Engineering an Efficient SAT Solver,”
in Proc. DAC, 2001, pp. 530-535.
[22] S. Reda and A. Salem, “Combinational Equivalence Checking Using
Boolean Satisfiability and Binary Decision Diagrams,” in Proc. DATE,
2001, pp. 122-126.
[23] G. S. Tseitin, “On the Complexity of Derivation in Propositional
Calculus,” in Studies in Constr. Math. and Math. Logic, 1968. pp. 115-
125.
[24] A. Veneris, et al. “Logic Verification based on Diagnosis Technique,” in
Proc. ASPDAC, 2003, pp. 538-543.
[25] S. C. Wu, et al., “Novel Probabilistic Combinational Equivalence Checking,”
IEEE TVLSI, vol. 16, pp. 365-375, April 2008.
[26] W. Wu and M. S. Hsiao, “Mining Global Constraints with Domain
Knowledge for Improving Bounded Sequential Equivalence Checking,”
IEEE TCAD, vol. 27, pp. 197-201, Jan. 2006.
[27] Q. Zhu, et al., “SAT Sweeping with Local Observability Don’t Cares,”
in Proc. DAC, 2006, pp. 229-234.
[28] http://iwls.org/iwls2005/benchmarks.html
[29] http://minisat.se/