- 學位論文
在可達狀態空間的相依正反器識別之研究
Dependent Latch Identification in the Reachable State Space
摘要
大量的正反器存在目前的設計會增加正規驗證和邏輯合成的複雜度。 主要的原因是隨著正反器數目的增加會使得狀態空間成指數性的成長。其中一種解決方法是找出正反器間的相依性。 如果知道正反器間的相依性，這些正反器就可以被分類成相依正反器和必要正反器這兩類，而且真正的狀態空間則由必要正反器所構成。 雖然有很多研究使用以BDD為基礎的象徵演算法去找尋這些正反器間的相依性，但是仍然無法有效的處理大型的循序電路。在這篇論文裡，我們使用SAT方法及Craig內插定理去尋找正反器間的相依性。 此外，我們所提出的方法還可以偵測出只存在可達狀態空間的循序相依性。經由循序相依性，我們可以偵測出額外的相依正反器存在於某個特定的時間框架之後，並且可以利用它們來達到額外的狀態空間減少。實驗結果顯示，這種方法可以在合理的時間內處理擁有一千五百以上個正反器的大型循序電路，並且找出它們組合及循序的相依正反器。例如，針對iscas'89測資裡的s13207，23%的正反器是組合相依正反器及額外的13%正反器是循序相依正反器。經由這些相依正反器的偵測，對s13207作可達性分析時，可以減少70.70%的BDD大小和73.32%的執行時間去達到相同的時間框架。除此之外，在600000秒的執行時間限制下，2890.76%的狀態空間也就是更多的狀態空間可以被達到。
並列摘要
The large number of latches in current designs increase the complexity of formal verification and logic synthesis. The reason for this is that the growth of latch number leads the state space to explode exponentially. One solution to this problem is to find the functional dependencies among these latches. With the identification of functional dependencies, these latches can be identified as dependent latches or essential latches, where the state space can be constructed using only the essential latches. Although much research has been devoted to exploring the functional dependencies among latches by BDD-based symbolic algorithms, this issue is still unresolved for large sequential circuits. In this work, we attempt to find the functional dependencies among latches in a sequential circuit by using SAT solvers with the Craig interpolation theorem. In addition, our proposed approach detects sequential functional dependencies existing in the reachable state space only. The sequential functional dependencies can identify additional dependent latches after a specific timeframe in order to achieve additional reduction of the state space. Experimental results show that this approach could deal with large sequential circuits with up to 1.5K latches in a reasonable time and simultaneously identify their combinational and sequential dependent latches. For instance, with s13207 in ISCAS’89, 23% of latches are identified as combinational dependent latches and an additional 13% of latches are identified as sequential dependent latches. For the reachability analysis of s13207, with the benefits of dependent latch identification, 70.70% of BDD size and 73.32% of CPU time can be reduced when reaching to the same timeframe. Furthermore, 2890.76% more states can be reached under 600, 000 run time limit.