江介宏臺灣大學：電子工程學研究所李崇閔Li, Chung-MinChung-MinLi2007-11-272018-07-102007-11-272018-07-102007http://ntur.lib.ntu.edu.tw//handle/246246/57272循序電路的驗證工作中，初始化是其中的一個重要議題，它確保電路能從正確的初始狀態開始運作。在此論文中，我們將致力於循序電路的初始化。更具體而言，我們欲確保循序電路能被正確地初始化且由外部硬體重置的暫存器數量最少，亦即，由內部訊號重置的暫存器數量最多。給定一初始化輸入信號序列的長度上限，我們可計算出一個由內部訊號重置暫存器的最大集合及其可行的初始化輸入信號序列。我們提出了二個新穎性的方法。第一個方法運用了結構基礎為導向的技術，我們呈現出以圖形理論來有系統地闡述外部硬體重置暫存器最小化的問題。不同長度限制的初始化輸入信號序列，對應到不同的圖形議題；第二個方法整合了結構基礎與狀態轉換基礎為導向的技術。因為在挑選了外部硬體重置的暫存器後，可使得初始化分析所需的記憶體空間降低，因此而減輕了狀態轉換數劇增的問題。實驗結果顯示我們所提方法的可行性。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.List of Figures vii List of Tables viii Acknowledgements (誌謝) ix 摘要 x Abstract xi 1 Introduction 1 1.1 Explicit-reset vs. implicit-reset register . . . . . . . . . . . . . . . . . 2 1.2 Previous work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Main contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4 Thesis organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2 Preliminaries 10 2.1 Sequential circuit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2 Finite state machine . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3 Binary decision diagram . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.4 Image computation and reachability analysis . . . . . . . . . . . . . . 18 2.5 Graph basics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3 Structural-Based Technique 24 3.1 Partial scan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.2 New approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.2.1 Problem formulation in input length 0 . . . . . . . . . . . . . 29 3.2.2 Problem formulation in input length 1 . . . . . . . . . . . . . 29 3.2.3 Problem formulation in input length k . . . . . . . . . . . . . 34 3.2.4 Problem formulation in unbounded length . . . . . . . . . . . 36 3.2.5 Optimization with simulated annealing . . . . . . . . . . . . . 40 3.3 Experimental result . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 4 Hybrid Technique 51 4.1 State-based method . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.1.1 Tree based resetability analysis . . . . . . . . . . . . . . . . . 52 4.1.2 Pixley’s resetability analysis . . . . . . . . . . . . . . . . . . . 52 4.2 New approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 4.3 Experimental result . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 4.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 5 Conclusion and Future Work 71 Bibliography1805349 bytesapplication/pdfen-US循序電路驗證初始化外部硬體重置內部訊號重置結構基礎狀態轉換基礎sequential circuitverificationinitializationexplicit-resetimplicitresetstructural-basedstate-basedthesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/57272/1/ntu-96-R94943150-1.pdf