在電路的合成、正規驗證和測試上，可達性分析都扮演了相當重要的角色。象徵性演算法，也就是利用二元決策圖來表示狀態的集合以及執行映像計算已經發展了十幾年，這些象徵性演算法都是以時間框架為基礎的，也就是一次將整個時間框架的映象算出來，然而，由於二元決策圖的大小呈現爆炸性的擴張，使得映像計算在較大的循序電路上變得相當棘手，因此，在可達性分析的問題裡，對每個時間框架都去計算完整的映像變得不切實際。本篇論文提出了一種新的以多狀態
為基礎的演算法來做可達性分析，此種演算法以類似分而治之的方式來進行可達性分析，盡量在有限的時間內到達最大的狀態，這種方法藉由反覆的執行部分的小的映像計算來取代龐大的映像計算，因此，每個映像計算的複雜度、ＣＰＵ時間和內存的使用都比較小。如此，在計算映象的過程中就不會卡在某個相當複雜且龐大的時間框架中。將實驗結果與ＶＩＳ作比較，此種做法可以達到更多的狀態在相同CPU時間並且使用較少的記憶體。

Reachability analysis is an important step in formal verification, synthesis, and testing of sequential circuits. Symbolic algorithms that represent state sets and
perform image computation by binary decision diagram (BDD) have been developed for more than one decade. Those symbolic methods are timeframe-based, i.e., performing image computation on the whole state set one timeframe after another timeframe. However, the image computation operation on large sequential circuits becomes more intractable due to explosive expansion of BDD size. Thus, computing the entire reachable state set in each timeframe becomes impractical in the reachability analysis. In this paper, we propose a novel cube-based algorithm that does not compute the complete reachable state set of each timeframe at a time. The cube-based algorithm traverses the state space in a divide-and-conquer manner to maximize the number of reached states with limited computation resources. This approach performs partial small image computations iteratively instead of one complete but huge image computation. As a result, the computation complexity of each iteration would be smaller, so does the CPU time and memory usage. Therefore, the reaching process would not get stuck in a certain timeframe in which image is too complex to be computed. As comparing the results with VIS, this approach could reach more states within the same CPU time and use less memory.

[1] 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
Conf., pp. 317-320, 1999.
[2] R. E. Bryant, “Graph-based algorithms for boolean function manipulation,” in
IEEE Trans. Computer, vol. C-35, pp. 677-691, 1986.
[3] R. K. Brayton et al, “VIS: A system for verification and synthesis,” in
Proc. Int. Conf. Computer-Aided Verification, pp. 423-427, 1996.
[4] H. Cho, G. D. Hatchel, E. Macii, B. Plessier, and F. Somenzi, “Algorithms
for approximate FSM traversal based on state space decomposition,”
in Proc. Int. Conf. on Design Automation, pp. 25-30, 1993.
[5] P. Chauhan, E. M. Clarke, and D. Kroening, “Using SAT-based image computation
for reachability analysis,” in Technical Report CMU-CS-03-151, Carnegie
Mellon University, 2003.
[6] O. Coudert, C. Berthet, and J. C. Madre, “Verification of synchronous sequential
machines based on symbolic execution,” in Proc. Computer-Adied Verification,
LNCS. 407, 1989.
[7] A. Gupta, Z. Yang, P. Ashar, and A. Gupta, “SAT–based image computation
with application in reachability analysis,” in Proc. Int. Conf. Formal Methods
in Computer-Aided Design, pp. 354-372, 2000.
[8] A. Gupta, Z. Yang, P. Ashar, L. Zhang, and S. Malik, “Partitionbased
decision heuristics for image computation using SAT and BDDs,” in
Proc. Int. Conf. Compute-Aided Design, pp. 286-292, 2001.
[9] S. G. Govindaraju, D. L. Dill, A. Hu, and M. A. Horowitz, “Approximate
reachability analysis with BDDs using overlapping projections,” in Proc. Design
Automation Conference, pp. 451-456 , 1998.
[10] R. Hojati, S. Krishnan, and R. K. Brayton. “Heuristic algorithms for early
quantification and partial product minimization,” in Technical Report M94/11,
UC Berkeley, 1994.
[11] R. Hojati, S. C. Krishnan, and R. K. Brayton, “Early quantification and partitioned
transition relations,” in Proc. Int. Conf. on Computer Design, pp. 12-19,
1996.
[12] N. Ishiura, H. Sawada, and S. Yajima, “Minimization of binary decision diagrams
based on exchanges of variables,” in Proc. Int. Conf. on Computer-Aided
Design, pp. 472-475, 1991.
[13] J. H. R. Jiang and R. K. Brayton, “On the verification of sequential equivalence,”
in IEEE Trans. Computer-Aided Design, pp. 686-697, 2003.
[14] R. Rudell, “Dynamic variable ordering for binary decision diagrams,” in
Proc. Int. Conf. on Computer-Aided Design, pp. 42-47, 1993.
[15] R. K. Ranjan, A. Adnan, R. K. Brayton, B. Plessier, and C. Pixley, “Efficient
BDD algorithms for FSM synthesis and verification,” Presented at IWLS’95:
IEEE International Workshop on Logic Synthesis, 1995.
[16] I. H. Moon, J. Y. Jang, G. D. Hacthtel, F. Somenzi, J. Yuan, and C. Pixley,
“Approximate reachability don’t cares for CTL model checking,” in
Proc. Int. Conf. on Computer-Aided Design, pp. 351-358, 1998.
[17] D. Stoffel, M. Wedler, P. Warkentin and W. Kunz, “Structural FSM traversal,”
in IEEE Trans. Computer-Aided Design, vol. 23, no. 5, pp. 598-619, 2004.
[18] D. Stoffel and W. Kunz, “Record & play: A structural fixed point iteration
for sequential circuit verification,” in Proc. Int. Conf. Computer-Aided Design,
pp. 394-399, 1997.
[19] E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha,
H. Savoj, P. R. Stephan, R. K. Brayton, and A. Sangiovanni-Vincentelli, “SIS: A
System for sequential circuit synthesis,” Technical Report UCB/ERL M92/41,
Electronics Research Lab, Univ. of California, Berkeley, CA 94720, 1992.
[20] F. Somenzi et al, “CUDD: university of colorado decision diagram package.”
http://vlsi.colorado.edu/˜fabio/CUDD