Please use this identifier to cite or link to this item:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/42661Full metadata record
| ???org.dspace.app.webui.jsptag.ItemTag.dcfield??? | Value | Language |
|---|---|---|
| dc.contributor.advisor | 黃鐘揚 | |
| dc.contributor.author | Ji-Han Liu | en |
| dc.contributor.author | 劉季涵 | zh_TW |
| dc.date.accessioned | 2021-06-15T01:19:03Z | - |
| dc.date.available | 2009-07-29 | |
| dc.date.copyright | 2009-07-29 | |
| dc.date.issued | 2009 | |
| dc.date.submitted | 2009-07-27 | |
| dc.identifier.citation | [1] Adrian Evan, Allan Siburt, Gary Vrckonik, Thane Brown, Mario Dufresne, Geoffrey Hall, Tung Ho and Ting Liu, “Functional Verification of Large ASICs”, 35th Design Automatic Conf., June 1998.
[2] Chien-Nan Liu and Jing-Yang Jou, “On Computer-Aided Techniques for Functional Verification of Complex Digital Designs”, PhD Dissertation, Department of Electronics and Institute of Electronics College of Electrical Engineering and Computer Science, National Chiao Tung University, May 2001. [3] Mike Benjamin, Daniel Geist, Alan Hartman, Yaron Wolfsthal, Gerard Mas, and Ralph Smeets, “A Study in Coverage-Driven Test Generation”, 36th Design Automatic Conf., June 1999. [4] Richard C. Ho and Mark A. Horowitz, “Validation Coverage Analysis for Complex Digital Designs”, Int’l Conf. on Computer Aided Design, Nov. 1996. [5] Dinos Moundanos, Jacob A. Abraham, and Yatin V. Hoskote, “Abstraction Techniques for Validation Coverage Analysis and Test Generation”, IEEE Trans. on Computer, Vol. 47, no. 1, pp. 2-14, Jan. 1998. [6] Michael C. McFarland, “Formal Verification of Sequential Hardware: A Tutorial”, IEEE Trans. on Computer-Aided Design of Integration Circuits and System, vol. 12, no. 5, pp.633-654, May 1993. [7] Vishnu C. Vamjamv, “Strategies for SAT-based Formal Verification”, PhD Dissertation, Department of Electrical and Computer Engineering, Virginia Polytechnic Institute and State University, Jan. 2007. [8] J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential Circuit Verification Using Symbolic Model Checking”, 27th Design Automatic Conf., June 1990. [9] H. Iwashita, T. Nakata, and F. Hirose, “CTL Model Checking Based on Forward State Traversal”, Int’l Conf. on Computer Aided Design, Nov. 1996. [10] Jerry R. Burch, Edmund M. Clarke, Davide E. Long, Kenneth L. McMillan, and David L. Dill, “Symbolic Model Checking for Sequential Circuit Verification”, IEEE Trans. on Computer-Aided Design, vol. 13, no. 4, pp.401-424, Apr. 1994. [11] Randal E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Trans. On Computers, pp. 677-691, Aug. 1986. [12] Aarti Gupta, Zijiang Yang, Pranav Ashar, Lintao Zhang and Sharad Malik, “Partition-Based Decision Heuristics for Image Computation using SAT and BDDs”. [13] Maher Mneimneh and Karem Sakallah, “SAT-based Sequential Depth Computation”. [14] Ralph Marczynski, Mitchell A. Thornton and Stephen A. Szygenda, “Test Vector Generation and Classification using FSM Traversals”, Department of Computer Science and Engineering, Southern Methodist University. [15] Shankar G. Govindaraju, David L. Dill and Jules P. Bergmann, “Implicit Approximate Reachability using Auxiliary State Variable”, Computer System Laboratory, Stanford University. [16] Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple and Fabio Somenzi, “Approximation and Decomposition of Binary Decision Diagrams”, 35th Design Automatic Conf., June 1998. [17] Michael L. Case, Alan Mishchenko and Robert K. Brayton, “Inductively Finding a Reachable State Space Over-Approximation”, Department of EECS, University of California, Berkeley. [18] Thomas Robert Shiple, “Formal Analysis of Synchronous Circuits”, PhD Dissertation, Graduate Division of Engineering-Electrical Engineering and Computer Sciences, University of California, Berkeley. [19] Tsu-Hua Wang and Chong Guan Tan, “Practical Code Coverage for Verilog”, Int’l Verilog HDL Conf., Mar. 1995. [20] Dean Darko and Paul Cohen, “HDL Verification Coverage”, Integrated Systems Design Magazine, June 1998. [21] Jing-Yang Jou and Chien-Nan Jimmy Liu, “Coverage Analysis Techniques for HDL Design Validation”, the 6th Asia Pacific Conf. on cHip Design Languages (APCHDL‘99), October 1999. [22] C.-N. Liu and J.-Y. Jou, “Efficient Coverage Analysis Metric for HDL Design Validation”, IEE Proceedings – Computers and Digital Techniques, vol. 148, no. 1, pp. 1-6, Jan. 2001. [23] Chen-Yi Chang, “On Functional Coverage Analysis for Circuit Description in HDL”, Master Thesis, Department of Electronics Engineering, National Chiao Tung University, 1999. [24] Gianpiero Cabodi and Paolo Camurati, “Symbolic FSM Traversals Based on the Transition Relation”, IEEE Trans. on Computer-Aided Design vol. 16, no. 5, pp.448-457, May 1997. [25] F. Somenzi, “CUDD: CU Decision Diagram Package”, http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html [26] K. S. Brace, R. L. Rudell, and R. E. Bryant. “Efficient Implementation of a BDD Package”, Design Automation Conference, 1990. [27] ABC: A System for Sequential and Verification, http://www.berkeley.edu/~alanmi/abc/ | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/42661 | - |
| dc.description.abstract | 由於電路設計日趨複雜化，電路正確性的驗證已是不可或缺的一個步驟。模擬是目前普遍用於驗證邏輯閘階層或暫存器移轉階層電路設計的功能的方法，然而這種方法對於人工輸入或隨機產生的模擬測試序列品質的評估，雖然已有數種涵蓋率的技術來作量化的比較，但是對於驗證完整度的評量，仍然缺乏一種具有足夠鑑別率的量化量度。因此在本論文中，我們以正規驗證技術的循序深度計算與可達性分析，推衍出可供設計者評估模擬測試序列品質與模擬涵蓋率的合理量度，並且亦修正前述量度以因應正規驗證在較大電路的運算資源不足問題。此外，本論文所提出的量度是根據循序深度的模擬正確度、限定模擬時間中布林狀態空間中狀態或cubes的模擬完整度、循序深度的模擬效能以及設計者加權等需求而決定。 | zh_TW |
| dc.description.abstract | Due to the increasing design complexity, verification of modern VLSI designs has become an essential work in the design flow. Simulation is predominant verification method to verify the functionality of gate level or register-transfer level (RTL) design nowadays. However, it lacks one quantitative metric with enough discrimination to verify the simulation completeness although there exist several coverage metrics for qualifying the test sequence manually defined or randomly generated in simulation. Accordingly, sequential depth computation and reachability analysis of the formal verification techniques are employed to derive or infer the feasible metrics for measuring the quality of test sequence and coverage of simulation. Hence, a modified version of the mentioned metric is proposed to overcome the problem of failure in sequential depth computation and BDD (binary decision diagrams) of transition relationship construction due to the system resource explosion. The proposed metrics consist of the requirements of simulation correctness of sequential depth, simulation completeness of states or cubes of Boolean state space in limited simulation timeframe, simulation performance of sequential depth and weighting in accordance with designer’s preference or concern of the simulation. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-15T01:19:03Z (GMT). No. of bitstreams: 1 ntu-98-P94921003-1.pdf: 700642 bytes, checksum: b8883a11367a1677adb70119c15ad233 (MD5) Previous issue date: 2009 | en |
| dc.description.tableofcontents | 誌謝 I
摘要 II Abstract III Table of Contents IV List of Figures VI List of Tables VII Chapter 1 Introduction 1 1.1 Simulation-Based and Formal-Based Verification 1 1.2 State Reachability of Simulation and Formal Approaches 4 1.3 Verification Quality 5 1.4 Organization of the Thesis 5 Chapter 2 Motivation of the Thesis 7 2.1 Limitation of Simulation-Based Verification 7 2.2 Limitation of Formal-Based Verification 8 2.3 Coverage Metrics 9 Chapter 3 Formal-based Functional Coverage Metrics 11 3.1 Definition of our Functional Coverage Metric 11 3.2 Definition of our Approximate Functional Coverage Metric 14 3.3 Algorithm Overview 15 3.4 Reachability Analysis 18 3.5 Simulation and Depth Collection 22 Chapter 4 Experimental Results 25 Chapter 5 Conclusions and Future Works 32 Reference 34 | |
| dc.language.iso | en | |
| dc.subject | 循序深度 | zh_TW |
| dc.subject | 可達性分析 | zh_TW |
| dc.subject | 模擬 | zh_TW |
| dc.subject | 涵蓋率量度 | zh_TW |
| dc.subject | 正規驗證 | zh_TW |
| dc.subject | 二元決策圖 | zh_TW |
| dc.subject | reachability analysis | en |
| dc.subject | Simulation | en |
| dc.subject | Formal Verification | en |
| dc.subject | BDD (Binary Decision Diagrams) | en |
| dc.subject | coverage metric | en |
| dc.subject | sequential depth | en |
| dc.title | 以正規方法驗證模擬測試序列品質 | zh_TW |
| dc.title | Qualify Simulation Test Sequence with Formal Method | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 97-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 陳朝欽,李建模 | |
| dc.subject.keyword | 模擬,正規驗證,二元決策圖,涵蓋率量度,循序深度,可達性分析, | zh_TW |
| dc.subject.keyword | Simulation,Formal Verification,BDD (Binary Decision Diagrams),coverage metric,sequential depth,reachability analysis, | en |
| dc.relation.page | 37 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2009-07-27 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
| Appears in Collections: | 電機工程學系 | |
Files in This Item:
| File | Size | Format | |
|---|---|---|---|
| ntu-98-1.pdf Restricted Access | 684.22 kB | Adobe PDF |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.