有限狀態機之整合初始化技術

Effective FSM Initialization Using Structural and State Based Reset

李崇閔(Chung-Min Li)

指導教授 ： 江介宏

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2007年)

https://doi.org/10.6342/NTU.2007.01003

摘要

循序電路的驗證工作中，初始化是其中的一個重要議題，它確保電路能從正確的初始狀態開始運作。在此論文中，我們將致力於循序電路的初始化。更具體而言，我們欲確保循序電路能被正確地初始化且由外部硬體重置的暫存器數量最少，亦即，由內部訊號重置的暫存器數量最多。給定一初始化輸入信號序列的長度上限，我們可計算出一個由內部訊號重置暫存器的最大集合及其可行的初始化輸入信號序列。我們提出了二個新穎性的方法。第一個方法運用了結構基礎為導向的技術，我們呈現出以圖形理論來有系統地闡述外部硬體重置暫存器最小化的問題。不同長度限制的初始化輸入信號序列，對應到不同的圖形議題；第二個方法整合了結構基礎與狀態轉換基礎為導向的技術。因為在挑選了外部硬體重置的暫存器後，可使得初始化分析所需的記憶體空間降低，因此而減輕了狀態轉換數劇增的問題。實驗結果顯示我們所提方法的可行性。

關鍵字

循序電路 ； 驗證 ； 初始化 ； 外部硬體重置 ； 內部訊號重置 ； 結構基礎 ； 狀態轉換基礎

並列摘要

Among the verification tasks of sequential circuits, FSM initialization is one of the most important problems. It ensures that a sequential circuit starts from a correct initial state. In this thesis, we are concerned with the initialization problem for sequential circuits. More specifically, we would like to ensure that a given sequential circuit is initialized properly while the number of explicit-reset registers is minimized or, equivalently, the number of implicit-reset registers is maximized. Essentially, given a length upper bound on the reset sequence, we compute a minimal set of explicit-reset registers along with a valid reset sequence of the circuit. We present two novel methods and techniques for initializing the circuit. The first method uses a structural-based technique. We show that the explicit-reset minimization problem can be formulated using graph theory. Depending on the upper bound of the reset-sequence length, minimizing explicit-reset registers may correspond to different graph problems. The second method uses a hybrid approach combining the structural-based method with Pixley’s resetability analysis of state-based method. Because the state traversal can be done in a reduced space with respect to a selected set of explicitreset registers, the state explosion problem can be much alleviated. Experiments show promising results for our proposed methods.

並列關鍵字

sequential circuit ； verification ； initialization ； explicit-reset ； implicitreset ； structural-based ； state-based

參考文獻

[1] C. Pixley. “A computational theory and implementation of sequential hardware equivalence.” In Proceedings DIMACS Workshop on Computer Aided Verification, pp. 293-320, 1991.

[2] C. Pixley. “A theory and implementation of sequential hardware equivalence.” IEEE Transactions on Computer-Aided Design, vol. 11, no. 13, pp. 1469-1478, Dec. 1992.

[4] J. K. Rho, F. Somenzi, and C. Pixley. “Minimum length synchronizing sequences of finite state machine.” In Proceeding Design Automation Conference, pp. 463-468, Jun 1993.

[5] C. Pixley, S. W. Jeong, and G. D. Hachtel. “Exact calculation of synchronizing sequences based on binary decision diagrams.” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 13, no.8, pp. 1024-1034, Aug. 1994.

[6] F. C. Hennie. Finite state models for logical machines. John Wiley Sons, Inc., 1968.