Skip navigation

DSpace

機構典藏 DSpace 系統致力於保存各式數位資料(如:文字、圖片、PDF)並使其易於取用。

點此認識 DSpace
DSpace logo
English
中文
  • 瀏覽論文
    • 校院系所
    • 出版年
    • 作者
    • 標題
    • 關鍵字
    • 指導教授
  • 搜尋 TDR
  • 授權 Q&A
    • 我的頁面
    • 接受 E-mail 通知
    • 編輯個人資料
  1. NTU Theses and Dissertations Repository
  2. 重點科技研究學院
  3. 積體電路設計與自動化學位學程
請用此 Handle URI 來引用此文件: http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/94514
完整後設資料紀錄
DC 欄位值語言
dc.contributor.advisor黃鐘揚zh_TW
dc.contributor.advisorChung-Yang Huangen
dc.contributor.author邱浤竣zh_TW
dc.contributor.authorHung-Chun Chiuen
dc.date.accessioned2024-08-16T16:28:57Z-
dc.date.available2024-08-17-
dc.date.copyright2024-08-16-
dc.date.issued2024-
dc.date.submitted2024-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.urihttp://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.abstractDeveloping 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.provenanceSubmitted by admin ntu (admin@lib.ntu.edu.tw) on 2024-08-16T16:28:56Z
No. of bitstreams: 0
en
dc.description.provenanceMade available in DSpace on 2024-08-16T16:28:57Z (GMT). No. of bitstreams: 0en
dc.description.tableofcontentsAcknowledgements 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.isoen-
dc.subject設計驗證zh_TW
dc.subject設計解析和合成zh_TW
dc.subject驗證工具zh_TW
dc.subject邏輯電路zh_TW
dc.subject正規驗證zh_TW
dc.subjectVerification Toolen
dc.subjectDesign Verificationen
dc.subjectFormal Verificationen
dc.subjectLogic Circuiten
dc.subjectDesign Parsing and Synthesisen
dc.title用於開發設計驗證演算法的通用驗證框架zh_TW
dc.titleA General-purpose Verification Framework for the Development of Design Verification Algorithmsen
dc.typeThesis-
dc.date.schoolyear112-2-
dc.description.degree碩士-
dc.contributor.oralexamcommittee黃紹倫;李建模;莊咸和zh_TW
dc.contributor.oralexamcommitteeShao-Lun Huang;Chien-Mo Li;Xian-Huo Zhuangen
dc.subject.keyword設計驗證,設計解析和合成,驗證工具,邏輯電路,正規驗證,zh_TW
dc.subject.keywordDesign Verification,Design Parsing and Synthesis,Verification Tool,Logic Circuit,Formal Verification,en
dc.relation.page58-
dc.identifier.doi10.6342/NTU202403562-
dc.rights.note未授權-
dc.date.accepted2024-08-12-
dc.contributor.author-college重點科技研究學院-
dc.contributor.author-dept積體電路設計與自動化學位學程-
顯示於系所單位:積體電路設計與自動化學位學程

文件中的檔案:
檔案 大小格式 
ntu-112-2.pdf
  未授權公開取用
6.88 MBAdobe PDF
顯示文件簡單紀錄


系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。

社群連結
聯絡資訊
10617臺北市大安區羅斯福路四段1號
No.1 Sec.4, Roosevelt Rd., Taipei, Taiwan, R.O.C. 106
Tel: (02)33662353
Email: ntuetds@ntu.edu.tw
意見箱
相關連結
館藏目錄
國內圖書館整合查詢 MetaCat
臺大學術典藏 NTU Scholars
臺大圖書館數位典藏館
本站聲明
© NTU Library All Rights Reserved