請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/94514完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 黃鐘揚 | zh_TW |
| dc.contributor.advisor | Chung-Yang Huang | en |
| dc.contributor.author | 邱浤竣 | zh_TW |
| dc.contributor.author | Hung-Chun Chiu | en |
| dc.date.accessioned | 2024-08-16T16:28:57Z | - |
| dc.date.available | 2024-08-17 | - |
| dc.date.copyright | 2024-08-16 | - |
| dc.date.issued | 2024 | - |
| dc.date.submitted | 2024-08-08 | - |
| dc.identifier.citation | [1] Robert K. Brayton and Alan Mishchenko. Abc: An academic industrial-strength verification tool. In International Conference on Computer Aided Verification, 2010.
[2] Alan Mishchenko. ABC: System for Sequential Logic Synthesis and Formal Verification. https://github.com/berkeley-abc/abc. Accessed: 2024-06-01. [3] Clifford Wolf, Johann Glaser, and Johannes Kepler. Yosys-a free verilog synthesis suite. 2013. [4] yosys - Yosys Open SYnthesis Suite. https://github.com/YosysHQ/yosys. Accessed: 2024-06-01. [5] Armin Biere. Aiger format and toolbox. http://fmv.jku.at/aiger/. [6] Veripool. Verilator: Open-source Verilog HDL simulator. https://www.veripool.org/wiki/verilator. Accessed: 2024-06-01. [7] Verilog Value Change Dump File Parser. https://github.com/ben-marshall/verilog-vcd-parser. Accessed: 2024-06-01. [8] Armin Biere, Alessandro Cimatti, Edmund Clarke, Ofer Strichman, and Yunshan Zhu. Bounded model checking. volume 58, pages 117 – 148, 12 2003. [9] Hyeong-Ju Kang and In-Cheol Park. Sat-based unbounded symbolic model checking. In Proceedings 2003. Design Automation Conference (IEEE Cat. No.03CH37451), pages 840–843, 2003. [10] Niklas Een, Alan Mishchenko, and Robert Brayton. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD), pages 125–134, 2011. [11] ICCAD CAD Contest 2021 Problem A. Functional ECO with Behavioral Change Guidance. https://iccad-contest.org/2021/Problems.html. Accessed: 2024-06-01. [12] Niklas Eén and Niklas Sörensson. An extensible sat-solver. In International conference on theory and applications of satisfiability testing, pages 502–518. Springer, 2003. [13] Niklas Sorensson and Niklas Een. Minisat v1. 13-a sat solver with conflict-clause minimization. SAT, 2005(53):1–2, 2005. [14] Gilles Audemard and Laurent Simon. Glucose: a solver that predicts learnt clauses quality. SAT, 01 2009 [15] Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986. [16] Chung-Yang Ric Huang. RicBDD - A simple yet decent Binary Decision Diagram package. https://github.com/ric2k1/RicBDD. Accessed: 2024-06-01. [17] K. L. McMillan. Interpolation and sat-based model checking. In Warren A. Hunt and Fabio Somenzi, editors, Computer Aided Verification, pages 1–13, Berlin, Heidelberg, 2003. [18] Ching-Zong Chang. Improving constrained random pattern generation by automatic design abstraction, 2022. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/94514 | - |
| dc.description.abstract | 隨著積體電路(IC)複雜度和規模的增加,開法有效率的驗證演算法已成為 IC 設計驗證中重要的一部分。儘管現有的開源驗證框架,如 ABC 和 Yosys 已經非 常成熟,但在易用性、文件編寫、程式可讀性和擴充性方面存在缺點,導致實作 地效率較低。本論文提出了一個新的通用驗證框架,該框架在整合這些工具的同 時,解決了它們原有的限制。我們的框架有以下幾個主要的貢獻。通過利用 ABC 和 Yosys 的功能,我們簡化了語法分析和合成階段,並提供了一個環境來擴充外 部引擎。我們實現了一個電路(DUV)的表示,儲存在兩個引擎(ABC, Yosys) 和我們的資料結構 (Circuit)。此外,我們開發了通用引擎,改善了 DUV 和驗證工 具之間的資料傳輸介面。我們還使用命令列介面,以操作我們框架中的功能。實 驗結果表明,我們的方法顯著提高了演算法的實作效率,對設計驗證領域做出了 重大貢獻。 | zh_TW |
| dc.description.abstract | Developing efficient verification algorithms has become essential in the IC design flow with the increasing complexity and scale of integrated circuits. Existing open-source verification frameworks, such as ABC and Yosys, though beneficial, present challenges in user-friendliness, documentation, coding complexity, and extensibility, leading to inefficiencies. This thesis proposes a new general-purpose verification framework that integrates these tools while addressing their limitations.
Our framework introduces several key contributions. By leveraging the capabilities of ABC and Yosys, we streamline the parsing and synthesis phases and provide an extensible environment for enhancing external engines. We implement a representation of the Design Under Verification (DUV), managing its information through two engines and our data structure, Circuit Manager. Additionally, we develop utility engines that improve communication and interface mechanisms between the DUV and verification tools. Furthermore, we introduce the command-line interface that facilitates effective communication between the applications and algorithms in our framework. Experimental results demonstrate that our method significantly improves implementation efficiency and substantially contributes to the field of design verification. | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2024-08-16T16:28:56Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2024-08-16T16:28:57Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | Acknowledgements i
中文摘要 ii Abstract iii Contents v List of Figures vii List of Tables ix Chapter 1 Introduction 1 1.1 Motivation 1 1.2 Contributions 3 1.3 Thesis Organization 4 Chapter 2 Background Knowledge 5 2.1 Third Party Tools and Engines Utilized in Our Framework 5 2.2 Simulation-Based Verification 6 2.3 Formal-Based Verification 7 2.4 Functional ECO Problem 7 2.5 And-Inverter Graphs 8 2.5.1 Combinational AIG 8 2.5.2 Sequential AIG 8 Chapter 3 Overview of General-Purpose Verification Framework 9 3.1 The Architecture of Our Framework 9 3.2 Design Parsing and Synthesis 11 3.3 Design and Implementation of Engine Managers 13 3.4 Representation of the DUV 18 3.4.1 Introduction to the Circuit Manager 19 3.4.2 The purpose of Circuit Manager 23 3.4.3 Conversion to the Circuit 23 3.5 Utility Engines for Verification 25 Chapter 4 Major Functionalities of the Framework 34 4.1 Commands for Data Access 35 4.2 Commands for Data Conversion 36 4.3 Commands for Simulation and Verification 38 4.4 Command Creation Flow 40 Chapter 5 Experimental Results 43 5.1 Case Study 1: Developing the BDD-based Verification Application 43 5.2 Case Study 2: Developing the Interpolation-Based Model Checker 46 5.3 Case Study 3: Developing the CRPG by Automatic Design Abstraction 49 Chapter 6 Conclusions and Future Work 53 6.1 Conclusions 53 6.2 Future Work 54 References 56 | - |
| 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 | Verification Tool | en |
| dc.subject | Design Verification | en |
| dc.subject | Formal Verification | en |
| dc.subject | Logic Circuit | en |
| dc.subject | Design Parsing and Synthesis | en |
| dc.title | 用於開發設計驗證演算法的通用驗證框架 | zh_TW |
| dc.title | A General-purpose Verification Framework for the Development of Design Verification Algorithms | en |
| dc.type | Thesis | - |
| dc.date.schoolyear | 112-2 | - |
| dc.description.degree | 碩士 | - |
| dc.contributor.oralexamcommittee | 黃紹倫;李建模;莊咸和 | zh_TW |
| dc.contributor.oralexamcommittee | Shao-Lun Huang;Chien-Mo Li;Xian-Huo Zhuang | en |
| dc.subject.keyword | 設計驗證,設計解析和合成,驗證工具,邏輯電路,正規驗證, | zh_TW |
| dc.subject.keyword | Design Verification,Design Parsing and Synthesis,Verification Tool,Logic Circuit,Formal Verification, | en |
| dc.relation.page | 58 | - |
| dc.identifier.doi | 10.6342/NTU202403562 | - |
| dc.rights.note | 未授權 | - |
| dc.date.accepted | 2024-08-12 | - |
| dc.contributor.author-college | 重點科技研究學院 | - |
| dc.contributor.author-dept | 積體電路設計與自動化學位學程 | - |
| 顯示於系所單位: | 積體電路設計與自動化學位學程 | |
文件中的檔案:
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-112-2.pdf 未授權公開取用 | 6.88 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。
