請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/61717完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 黃鐘揚(Chung-Yang (Ric) | |
| dc.contributor.author | Kuan-Chang Wang | en |
| dc.contributor.author | 王冠璋 | zh_TW |
| dc.date.accessioned | 2021-06-16T13:10:37Z | - |
| dc.date.available | 2013-07-31 | |
| dc.date.copyright | 2013-07-31 | |
| dc.date.issued | 2012 | |
| dc.date.submitted | 2013-07-31 | |
| dc.identifier.citation | [1] IEEE Standard 1666 SystemC Language Reference Manual, 2005. www.systemc.org.
[2] D. C. Black and J. Donovan. SystemC: From the Ground Up. Springer, 2004. [3] B. Bailey, G. Martin and A. Piziali, ESL Design and Verification: A Prescription for Electronic System Level Methodology. Morgan Kaufmann/Elsevier. 2007 [4] A. Cimatti, A. Micheli, I. Narasamdya, M. Roveri. Verifying SystemC: a software model checking approach. In Proc. FMCAD, 2010. [5] A. Cimatti, I. Narasamdya, and M. Roveri. Boosting Lazy Abstraction for SystemC with Partial Order Reduction. In Proc. TACAS 2011. [6] A. Cimatti, I. Narasamdya, and M. Roveri. Verifying Parametric System Designs. In Proc. FMCAD 2012. [7] C.-N. Chou, C.-Y. Huang. Towards Formal Verification on SystemC designs.. Ph.D Dissertation NTU. 2013. [8] C.-N. Chou, C.-H. Hsu, Y.-T. Chao, and C.-Y. Huang. Formal deadlock checking on high-level SystemC designs. In Proc. ICCAD, 2010. [9] C.-N. Chou, Y.-S. Ho, C. Hsieh., and C.-Y. Huang. Symbolic model checking on SystemC designs. In Proc. DAC. 2012 [10] N. Een, A. Mishchenko, R. Brayton. Efficient Implementation of Property Directed Reachability. In Proc. FMCAD, 2011. [11] Hardware Model Checking Competition 2010. http://fmv.jku.at/hwmcc10/ [12] A. R. Bradley. SAT-based model checking without unrolling. In Proc. VMCAI, 2011 [13] A. R. Bradley and Z. Manna. Checking safety by inductive generalization of counterexamples to induction. In Proc. FMCAD, 2007. [14] F., Somenzi, A. R. Bradley. IC3: Where Monolithic and Incremental Meet. In Proc. FMCAD, 2011 [15] R. Brummayer and A. Biere. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In Proc. TACAS, 2009. [16] R. Brummayer, A. Biere and F. Lonsing. BTOR: bit-precise modeling of word-level problems for model checking. In Proc. BPR, 2008 [17] C. Girault and R. Valk. Petri Nets for System Engineering: A guide to Modeling, Verification, and Applications. Springer, 2002. [18] G. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, 1968. [19] Competition on Software Verification 2012. http://sv-comp.sosy-lab.org/2012/index.php [20] S. Hazelhurst and C.-J.H. Seger. Symbolic Trajectory Evaluation. In Formal Hardware Verification: Methods and Systems in Comparison. 1996. [21] A. Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani. The MathSAT5 SMT Solver. In Proc. TACAS 2013. [22] N. Een, and N. Sorensson. MiniSat - A SAT Solver with conflict-clause minimization, In Proc. SAT 2005. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/61717 | - |
| dc.description.abstract | 現今在System-on Chip的許多模組是以高階語言所描述完成, 然而在高階語言中, SystemC以它高效能的速度脫穎而出, 成為業界所認定的標準高階語言, 也因為如此, 在IC晶片設計流程中, SystemC 的設計驗證是非常重要且關鍵.
在這篇論文中, 我們以正規方法定義狀態變數並且以完全符號化模擬建立出變換聯繫, 在我們的正規模組之下, 我們能夠較容易地去實現其他軟硬體上的技術, 並且考慮SystemC上各個角度下的許多語意. 另一方面, 我們也運用無邊際模組檢驗的演算法去驗證SystemC的設計, 然而我們在要將這個演算法轉換到高階語言中遇到許多挑戰, 因此我們也提出許多技術去克服這些困難, 最後, 實驗數據顯示出我們演算法的效能和能夠掌握的設計大小. | zh_TW |
| dc.description.abstract | Nowadays, most of executable models of System-on-Chip are written in high-level languages. Among all high-level description languages, SystemC is an industrial standard and has advantages of its high simulation speed. Therefore, verifying SystemC designs is significant and critical in the design process.
In this thesis, we formally define state variables and compute the transition relation of SystemC designs by fully symbolic simulation. With our formal model, we make it easier to apply other formal hardware/software verification techniques on SystemC verification while keeping lots of semantics aspects. On the other hand, we realize an unbounded model checking algorithm, Property-Directed Reachability (PDR), on SystemC verification. However, adopting the PDR algorithm on high-level design verification meets some challenges due to the different language environment. We present many techniques to overcome those difficulties in this thesis. The experimental results show the scalability and the efficiency of our methods. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-16T13:10:37Z (GMT). No. of bitstreams: 1 ntu-101-R00943094-1.pdf: 3711197 bytes, checksum: 99bbb724cbab9a7c151e2de65ec67b32 (MD5) Previous issue date: 2012 | en |
| dc.description.tableofcontents | 口試委員審定書 i
誌謝 ii 中文摘要 iii ABSTRACT iv CONTENTS v LIST OF FIGURES viii LIST OF TABLES ix Chapter 1 Introduction 1 1.1 Motivation 2 1.2 Contributions of this Thesis 3 1.3 Organization of this Thesis 4 Chapter 2 Preliminaries 5 2.1 SystemC 5 2.1.1 SystemC Semantics 5 2.1.2 SystemC Simulation Kernel 6 2.2 Our Multi-layer Modeling Framework 8 2.2.1 Extended Petri Net 8 2.2.2 Predictive Synchronization Dependence Graph 9 2.2.3 Our Simulation Kernel 10 2.3 Symbolic Simulation and Behavioral States 11 2.4 Overview of Property-Directed Reachability 14 2.4.1 Notations 14 2.4.2 Algorithm 15 Chapter 3 Formal Modeling for SystemC Verification 17 3.1 Assumptions 17 3.2 State Variables 18 3.3 State Transition Relation 21 3.4 Transition Boundary 22 Chapter 4 Property-Directed Reachability on SystemC Designs 24 4.1 Difficulties and Challenges of SystemC PDR 24 4.2 Overview of Our SystemC Verification Flow 26 4.2.1 Preprocess: Bounded Model Checking 27 4.2.2 Computing the Transition Relation by Fully Symbolic Simulation 28 4.2.3 SystemC PDR flow 31 4.3 SMT Solving 33 4.4 A Running Example 34 Chapter 5 Implementation Details 37 5.1 Data Structure of Implementation 37 5.2 Handling of Partial Unknown Bits for SMT Solver 39 5.3 Generalizations 40 5.4 Syntactical and Semantic Subsumptions 42 5.5 PDR Timeframe Folding 43 5.6 Propagation and Termination 44 Chapter 6 Experimental Results 46 6.1 Results of Deadlock Checking 47 6.2 Results of Assertion Checking 49 6.3 Profile and Analysis of PDR approach 50 Chapter 7 Conclusion and Future Work 52 REFERENCE 54 | |
| dc.language.iso | zh-TW | |
| dc.subject | SystemC | zh_TW |
| dc.subject | 正規SystemC 驗證 | zh_TW |
| dc.subject | 正規模組 | zh_TW |
| dc.subject | 完全符號化模擬 | zh_TW |
| dc.subject | 性質導向可達度技術 | zh_TW |
| dc.subject | formal SystemC verification | en |
| dc.subject | Property-Directed Reachability | en |
| dc.subject | fully symbolic simulation | en |
| dc.subject | SystemC | en |
| dc.subject | formal model | en |
| dc.title | 利用性質導向可達度技術進行正規SystemC設計驗證 | zh_TW |
| dc.title | Formal SystemC Verification based on Property-Directed Reachability | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 101-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 蔡仁松(Ren-Song Tsay),王柏堯(Bow-Yaw Wang),洪士灝(Shih-Hao Hung) | |
| dc.subject.keyword | SystemC,正規SystemC 驗證,正規模組,完全符號化模擬,性質導向可達度技術, | zh_TW |
| dc.subject.keyword | SystemC,formal SystemC verification,formal model,fully symbolic simulation,Property-Directed Reachability, | en |
| dc.relation.page | 55 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2013-07-31 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
| 顯示於系所單位： | 電子工程學研究所 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-101-1.pdf 未授權公開取用 | 3.62 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。