序向電路之可達性分析｜國立清華大學博碩士論文庫

簡易檢索 / 詳目顯示

回結果列表

研究生：	蔡榮泰 Jung-Tai Tsai
論文名稱：	序向電路之可達性分析 Reachability Analysis of Sequential Circuits
指導教授：	王俊堯 Chun-Yao Wang
口試委員:
學位類別：	碩士 Master
系所名稱：	電機資訊學院 - 資訊工程學系 Computer Science
論文出版年：	2007
畢業學年度：	95
語文別：	中文
論文頁數：	30
中文關鍵詞：	可達性
外文關鍵詞：	reachability
相關次數：	點閱：2 下載：0
分享至:	分享至facebook 分享至twitter

查詢本校圖書館目錄查詢臺灣博碩士論文知識加值系統勘誤回報

可達性分析對於超大型積體電路的合成和驗證而言是一項基礎且十份重要的技術。本篇論文提出一個創新且半正規的方法來走訪有限狀態機中的狀態，而這個方法同時結合了模擬和正規方法的優點。我們使用一系列ISCAS＇89的測資來進行實驗，並且與一個以偏移亂數方式為基礎的研究方法做比較，而實驗結果指出我們的方法的確能較有效率地得到更多的狀態數。

Reachability analysis is a fundamental technique in the Synthesis and verification of VLSI circuits. This paper presents a novel semi-formal approach which combines the advantages of simulation and formal methods to traverse the state space of the FSMs. We conduct the experiments on a set of ISCAS’89 benchmarks. As compared with a previous work which relies on biased random technique, our approach reaches more states with less CPU time.

摘要.......................................................i
Abstract..................................................ii
Acknowledgements.........................................iii
Contents..................................................iv
List of Figures...........................................vi
List of Tables...........................................vii

Chapter 1 Introduction.....................................1
1.1 Motivation.............................................1
1.2 Problem Formulation....................................2
1.3 Existing Approaches to Reachability Analysis...........2
1.4 Our Contributions......................................4
1.5 Overview...............................................4

Chapter 2 Background.......................................5
2.1 Set Representation.....................................5
2.2 State Set Representation...............................6
  2.2.1 Representation of Circuit States...................6
  2.2.2 Global BDD and Local BDD...........................7
2.3 Search Frontier........................................8
2.4 Random Pattern Generator (RPG).........................9
2.5 Controllability.......................................10

Chapter 3 Our Approach....................................11
3.1 Parallel Random Pattern Simulation....................11
3.2 Backward Justification................................14
  3.2.1 Forward Implication...............................15
  3.2.2 Justification Ordering............................15
  3.2.3 Controllability as A Guidance of Backtrace........17
3.3 Overall Flow..........................................20

Chapter 4 Experimental Results and Analysis...............22

Chapter 5 Conclusions.....................................27

Reference.................................................28

                                

References
[1] J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill, “Symbolic model checking for sequential circuit verification,” IEEE Trans. Computer-Aided Design,
vol. 13, no. 4, pp. 401-424, Apr. 1994.

[2] J. R. Burch, E. M. Clarke, and D. E. Long“Representing circuits more efficiently in symbolic model checking,” in Proc. 28th Design Automation Conf., pp. 403-407, 1991.

[3] J. R. Burch, E. M. Clarke, and D. E. Long, “Symbolic model checking with partitioned transition relations,” in Proc. Int. Conf. Very Large Scale Integration, pp. 49-58,
1991.

[4] J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential circuit verification using symbolic model checking,” in Proc. 27th Design Automation Conf.,
pp. 46-51, 1990.

[5] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic model checking: 10^20 states and beyond,” in Proc. Fifth Ann. IEEE Symp. Logic in Computer Sci., pp. 428-439, 1990.

[6] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic model checking: 10^20 states and beyond,” Infor. Computation, vol. 98, no. 2, pp. 142-
170, June 1992.

[7] O. Coudert, C. Berthet, and J. C. Madre, “Verification of synchronous sequential machines based on symbolic execution,” in Int. Workshop on Automatic Verification
Methods for Finite State Systems, pp. 365-373, June 1989.

[8] O. Coudert and J. C. Madre, “A unified framework for the formal verification of sequential circuits,” in Proc. Int. Conf. Computer-Aided Design, pp. 126-129, Nov. 1990.

[9] Y.-M. Kuo, C.-H. Lin, C.-Y. Wang, S.-C. Chang, and P.-H. Ho, “Intelligent random vector generator based on probability analysis of circuit structure,” in Proc. of
Int. Symp. Quality Electronic Design, pp. 344-349, 2007.

[10] D. Stoffel, M. Wedler, P. Warkentin, and W. Kunz,“Structural FSM Traversal,” IEEE Trans. Computer-Aided Design, vol. 23, no. 5, pp. 598-619, May 2004.

[11] 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, May 1992.

[12] H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, “Implicit state enumeration of finite state machines using BDD’s,” in Proc. Int. Conf. Computer-Aided Design, pp. 130-133, Nov. 1990.

[13] http://www.swox.com/gmp

全文公開日期本全文未授權公開 (校內網路)
全文公開日期本全文未授權公開 (校外網路)

簡易檢索 / 詳目顯示

相關論文