請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/53796
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang Huang) | |
dc.contributor.author | Chia-Hung Lin | en |
dc.contributor.author | 林佳鴻 | zh_TW |
dc.date.accessioned | 2021-06-16T02:29:56Z | - |
dc.date.available | 2020-08-03 | |
dc.date.copyright | 2015-08-03 | |
dc.date.issued | 2015 | |
dc.date.submitted | 2015-07-31 | |
dc.identifier.citation | [1] Kai-Hui Chang, Ilya Wanger, Valeria Bertacco and Igor L. Markov, “Automatic Error Diagnosis and Correction for RTL Designs,” In High Level Design Validation and Test Workshop 2007.
[2] Verdi, https://www.synopsys.com/Tools/Verification/debug/Pages/Verdi-ds.aspx [3] Kai-Hui Chang, Igor L. Markov and Valeria Bertacco, “Fixing Design Errors with Counterexamples and Resynthesis”, In Asia and South Pacific Design Automation Conference (ASP-DAC) 2007. [4] Alexander Smith, Andreas Veneris and Anastasios Viglas, “Design Diagnosis Using Boolean Satisfiability”, In Asia and South Pacific Design Automation Conference (ASP-DAC) 2004. [5] Gorschwin Fey, Stefan Staber, Roderick Bloem and Rolf Drechsler, “Automatic Fault Localization for Property Checking”, In Spring-Verlag LNCS 2007. [6] Stefan Staber, Barbara Jobstmann, and Roderick Bloem, “Finding and Fixing Faults” In Spring-Verlag LNCS 2005. [7] Andrew DeOrio, Adam B. Bauserman, Valeria Bertacco and Beth C. Isaksen, “Inferno: Streamlining Verification With Inferred Semantics”, In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD) 2009. [8] Hanne Riis Nielson and Chris Hankin Flemming Nielson, “Principles of program analysis”. [9] Toby Segaran, Colin Evans and Jamie Taylor, “Programming the Semantic Web”. [10] Chia-Hsun Cheng and Chung-Yang (Ric) Huang, “RTL-to-TL Model Generation Based on Protocol Abstraction Techniques”. [11] ANTLR (Another Tool for Language Recognition) by Terence Parr, et al. [Online]. Available: http://www.antlr.org/ [12] “Jess” Rule Engine. Available: http://www.jessrules.com/jess/index.shtml [13] QuickCores, http://www.quickcores.com/ [14] Fu-Chieh Chang and Chung-Yang (Ric) Huang, “A Formal Logic Approach to Chinese Recognizing Textual Entailment”. [15] Yueh-Tung Chao and Chung Yang (Ric) Huang, “Utilizing High-Level Synthesis Techniques in High-Level to RT-Level Equivalence Checking”. [16] Bijan Alizadeh, “A Formal Approach to Debug Polynomial Datapath Designs”, In Asia and South Pacific Design Automation Conference (ASP-DAC) 2012. [17] Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury and Satish Chandra, “SemFix: Program Repair via Semantic Analysis”, In International Conference on Software Engineering (ICSE) 2013. [18] Maksin Jenihhin, Anton Tsepurov, Valentin Tihhomirov, Jaan Raik, Hanno Hantson and Raimund Ubar, “Automated Design Error Localization in RTL Design”, In IEEE Design & Test 2013. [19] Tai-Ying Jiang, Chien-Nan Jimmy Liu and Jing-Yang Jou, “Effective Error Diagnosis for RTL Designs in HDLs”, In Asian Test Symposium 2002. [20] IEEE Standard for Verilog Hardware Description Language. IEEE Standard 1364, 2001. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/53796 | - |
dc.description.abstract | 暫存器轉換層級設計的除錯與驗證一直是個很有挑戰的問題,傳統的除錯方式常使用將多工器插入設計中以找出可能發生錯誤的位置。然而,因為設計的複雜度以及工程師本身對設計知識的了解,大部分工程師選擇藉由觀察波型圖找出可能的錯誤而非使用自動診斷及除錯工具。若能在除錯及驗證上整合人類的使用行為及知識將會是一個值得研究的方向。
我們提出一個新方法以及建構一個系統以對暫存器轉換層級進行除錯,就像平常工程師所習慣的藉由引進設計知識的正規語意模型及推論來除錯。透過程式語言以及設計知識的語意我們可以容易的找出可能發生錯誤的位置,此外我們也可以使用語意模型及設計知識將確認及監視自動地寫入設計中,最後,我們得出這個系統的優缺點,以及未來可行的研究方向來改進此系統。 | zh_TW |
dc.description.abstract | RTL (Register Transaction Level) design debugging and verification is always a challenging problem. Traditionally, the research of debugging used to insert MUX (Multiplexer) into design to find the bugs. However, because of the complexity and designer’s design knowledge of RTL design, most engineers used to use waveform tools (e.g. Verdi) with design knowledge to debug rather than using automatic debugging tool. Combining the human’s behavior and knowledge on debugging and verification is a good perspective to research.
We proposes a new approach and builds a system to debug RTL design by introducing formal semantic model and inference with design knowledge just like what designers used to do. With semantic of RTL code, design knowledge, we can easily infer what may cause these bugs. Also, we can use this semantic model and design knowledge to automatically write assertion and monitor into design. Finally, we point out the strengths and weaknesses of this approach, and possibilities on future research to improve our system. | en |
dc.description.provenance | Made available in DSpace on 2021-06-16T02:29:56Z (GMT). No. of bitstreams: 1 ntu-104-R02921029-1.pdf: 536830 bytes, checksum: 8b6cdb7eb6e90a8ea57ef41732b471e7 (MD5) Previous issue date: 2015 | en |
dc.description.tableofcontents | 口試委員會審定書............................................i
誌謝......................................................ii 中文摘要.................................................iii ABSTRACT..................................................iv CONTENTS...................................................v LIST OF FIGURES..........................................vii LIST OF TABLES............................................ix Chapter 1 Introduction...............................1 1.1 Related Works......................................2 1.2 Contributions of the Thesis........................2 1.3 Organization of the Thesis.........................3 Chapter 2 Preliminaries..............................4 2.1 Control Data Flow Graph............................4 2.2 Finite State Machine...............................8 2.3 Feed-Forward Inference.............................8 Chapter 3 Formal Semantic Model.....................10 3.1 Code Semantic.....................................11 3.2 Design Knowledge..................................14 Chapter 4 Implementation: System Architecture and Algorithm.................................................18 4.1 Overview..........................................18 4.2 Register Transaction Level Design Parser..........25 4.3 Semantic Constructor..............................27 4.4 Inference Engine and Assertion/Monitor Generator..32 Chapter 5 Implementation Issues.....................35 5.1 Code Flow Model...................................35 5.2 Semantic of Operators.............................35 5.3 Formal Semantic Model.............................36 5.4 Verification by Design Over-Approximate...........37 Chapter 6 Experimental and Case Study...............38 6.1 Case Study – Vending Machine......................40 6.2 Case Study –Multi Cycle MIPS......................44 6.3 Case Study – Neural Spiking Simulator.............47 6.4 Case Study – 8051.................................49 Chapter 7 Conclusions and Future Work...............51 7.1 Conclusions.......................................51 7.2 Future Work.......................................52 REFERENCE.................................................55 | |
dc.language.iso | en | |
dc.title | 暫存器轉換層級設計之除錯與驗證藉由設計知識之正規語意模型與推論 | zh_TW |
dc.title | RTL Design Debugging and Verification by Formal Semantic Modeling and Inference of Design Knowledge | en |
dc.type | Thesis | |
dc.date.schoolyear | 103-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 李建模(Chien-Mo Li),江介宏(Jie-Hong Jiang),王凡(Farn Wang) | |
dc.subject.keyword | 除錯,驗證,正規語意模型,語意推論,暫存器轉換層級, | zh_TW |
dc.subject.keyword | Debugging,Verification,Formal Semantic Model,Semantic Inference,Register Transaction Level, | en |
dc.relation.page | 56 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2015-07-31 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
顯示於系所單位: | 電機工程學系 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-104-1.pdf 目前未授權公開取用 | 524.25 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。