Skip navigation

DSpace JSPUI

DSpace preserves and enables easy and open access to all types of digital content including text, images, moving images, mpegs and data sets

Learn More
DSpace logo
English
中文
  • Browse
    • Communities
      & Collections
    • Publication Year
    • Author
    • Title
    • Subject
    • Advisor
  • Search TDR
  • Rights Q&A
    • My Page
    • Receive email
      updates
    • Edit Profile
  1. NTU Theses and Dissertations Repository
  2. 電機資訊學院
  3. 電機工程學系
Please use this identifier to cite or link to this item: http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/53796
Full metadata record
???org.dspace.app.webui.jsptag.ItemTag.dcfield???ValueLanguage
dc.contributor.advisor黃鐘揚(Chung-Yang Huang)
dc.contributor.authorChia-Hung Linen
dc.contributor.author林佳鴻zh_TW
dc.date.accessioned2021-06-16T02:29:56Z-
dc.date.available2020-08-03
dc.date.copyright2015-08-03
dc.date.issued2015
dc.date.submitted2015-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.urihttp://tdr.lib.ntu.edu.tw/jspui/handle/123456789/53796-
dc.description.abstract暫存器轉換層級設計的除錯與驗證一直是個很有挑戰的問題,傳統的除錯方式常使用將多工器插入設計中以找出可能發生錯誤的位置。然而,因為設計的複雜度以及工程師本身對設計知識的了解,大部分工程師選擇藉由觀察波型圖找出可能的錯誤而非使用自動診斷及除錯工具。若能在除錯及驗證上整合人類的使用行為及知識將會是一個值得研究的方向。
  我們提出一個新方法以及建構一個系統以對暫存器轉換層級進行除錯,就像平常工程師所習慣的藉由引進設計知識的正規語意模型及推論來除錯。透過程式語言以及設計知識的語意我們可以容易的找出可能發生錯誤的位置,此外我們也可以使用語意模型及設計知識將確認及監視自動地寫入設計中,最後,我們得出這個系統的優缺點,以及未來可行的研究方向來改進此系統。
zh_TW
dc.description.abstractRTL (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.provenanceMade 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.isoen
dc.subject驗證zh_TW
dc.subject暫存器轉換層級zh_TW
dc.subject除錯zh_TW
dc.subject語意推論zh_TW
dc.subject正規語意模型zh_TW
dc.subjectDebuggingen
dc.subjectRegister Transaction Levelen
dc.subjectSemantic Inferenceen
dc.subjectFormal Semantic Modelen
dc.subjectVerificationen
dc.title暫存器轉換層級設計之除錯與驗證藉由設計知識之正規語意模型與推論zh_TW
dc.titleRTL Design Debugging and Verification by Formal Semantic Modeling and Inference of Design Knowledgeen
dc.typeThesis
dc.date.schoolyear103-2
dc.description.degree碩士
dc.contributor.oralexamcommittee李建模(Chien-Mo Li),江介宏(Jie-Hong Jiang),王凡(Farn Wang)
dc.subject.keyword除錯,驗證,正規語意模型,語意推論,暫存器轉換層級,zh_TW
dc.subject.keywordDebugging,Verification,Formal Semantic Model,Semantic Inference,Register Transaction Level,en
dc.relation.page56
dc.rights.note有償授權
dc.date.accepted2015-07-31
dc.contributor.author-college電機資訊學院zh_TW
dc.contributor.author-dept電機工程學研究所zh_TW
Appears in Collections:電機工程學系

Files in This Item:
File SizeFormat 
ntu-104-1.pdf
  Restricted Access
524.25 kBAdobe PDF
Show simple item record


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

社群連結
聯絡資訊
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