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