請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/62055完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 黃鐘揚(Chung-Yang (Ric) | |
| dc.contributor.author | Chen-Kai Chu | en |
| dc.contributor.author | 朱振愷 | zh_TW |
| dc.date.accessioned | 2021-06-16T13:25:21Z | - |
| dc.date.available | 2013-07-30 | |
| dc.date.copyright | 2013-07-30 | |
| dc.date.issued | 2013 | |
| dc.date.submitted | 2013-07-23 | |
| dc.identifier.citation | [1] IEEE Standard 1666 SystemC Language Reference Manual, 2011. www.systemc.org.
[2] D. Tabakov, M. Y. Vardi, G. Kamhi, and E. Singerman, “A Temporal Language for SystemC,” In Proc. of FMCAD, 2008. [3] P. Herber, J. Fellmuth, and S. Glesner, “Model Checking SystemC Designs Using Timed Automata,” In Proc. of CODES+ISSS, 2008 [4] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “Uppaal — a Tool Suite for Automatic Verification of Real–Time Systems,” In Workshop on Verification and Control of Hybrid Systems, 1995. [5] D. Grose, H. M. Le, and R. Drechsler, “Proving Transaction and System-level Properties of Untimed SystemC TLM Designs,” In Proc. of MEMOCODE, 2010. [6] A. Cimatti, A. Micheli, I. Narasamdya, M. Roveri, “Verifying SystemC: a Software Model Checking Approach,” In Proc. of FMCAD, 2010. [7] E. M. Clarke, D. Kroening, and F. Lerda, “A tool for checking ANSI-C programs,” In Proc. of TACAS, 2004. [8] C.-N. Chou, Y.-S. Ho, C. Hsieh, and C.-Y. Huang, “Symbolic Model Checking on SystemC Desings,” In Proc. of DAC, 2012 [9] A. Cimatti, I. Narasamdya, and M. Roveri, “Boosting Lazy Abstraction for SystemC with Partial Order Reduction,” In Proc. of TACAS, 2011. [10] A. Cimatti, I. Narasamdya, and M. Roveri, “Verifying Parametric System Designs,” In Proc. of FMCAD, 2012. [11] C. Helmstetter, F. Maraninchi, L. Maillet-Contoz, and M. Moy, “Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip,” In Proc. of FMCAD, 2006. [12] S. Kundu, M. Ganai, and R. Gupta, “Partial Order Reduction for Scalable Testing of SystemC TLM Designs,” In Proc. of DAC, 2008. [13] N. Blanc and D. Kroening, “Race Analysis for SystemC using Model Checking,” In TODAES, Volume 15 Issue 3, May 2010. [14] C. Flanagan and P. Godefroid, “Dynamic Partial-Order Reduction for Model Checking Software,” In Proc. of POPL, 2005 [15] P. Godefroid. “Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem,” PhD thesis, Univerite De Liege, 1995. [16] M. Y. Vardi, “Formal Techniques for SystemC Verification,” In Proc. of DAC, 2007 [17] D. Kroening and N. Sharygina, “Formal Verification of SystemC by Automatic Hardware/Software Partitioning,” In Proc. of MEMOCODE, 2005. [18] C.-N. Chou, C.-H. Hsu, Y.-T. Chao, and C.-Y. Huang, “Formal Deadlock Checking on High-Level SystemC Designs,” In Proc. of ICCAD, 2010 [19] C.-N. Chou, “Towards Formal Verification on SystemC Designs,” PhD thesis, National Taiwan University, 2013. [20] J. Peterson, “Petri Net Theory and the Modeling of Systems,” Prentice Hall PTR, Upper Saddle River, NJ, USA, 1981 [21] V. Kahlon, C. Wang, and A. Gupta, “Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique,” In Proc. of CAV, 2009 [22] J. C. King, “Symbolic Execution and Program Testing,” In Commun. ACM, 1976. [23] A. Koelbl, J. Kukula, and R. Damiano, “Symbolic RTL Simulation,” In Proc. of DAC, 2001. [24] A. Koelbl and C. Pixley, “Constructing Efficient Formal Models from High-Level Descriptions using Symbolic Simulation,” In International Journal of Parallel Programming, 2005. [25] C. Pasareanu and W. Visser. “Verification of Java Programs Using Symbolic Execution and Invariant Generation,” In Proc. of 11th Int’l SPIN Workshop on Model Checking Software, volume 2989 of LectureNotes in Computer Science, pages 164–181. Springer, 2004. [26] A. W. Mazurkiewicz, “Trace theory,” In Advances in Petri Nets, pages 279–324. Springer, 1986. LNCS 255. [27] R. Brummayer and A. Biere, “Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays,” In Proc. of TACAS, 2009. [28] N. Een and N. Sӧrensson, “An Extensible SAT-Solver,” In Proc. of SAT, 2003. [29] Competition on Software Verification (SV-COMP’13), in TACAS, 2013. http://sv-comp.sosy-lab.org/2013/ | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/62055 | - |
| dc.description.abstract | 由於SystemC排程器容許在排程上的不確定性，SystemC的正規驗證被迫使處理在設計驗證上的可擴展性問題。這個可擴展性問題來自於探索所有可能的排程選擇，以確保能完整的捕捉到所有設計中可能的行為。為了能解決在探索排程選擇過程中造成的記憶體容量爆炸問題，我們在我們以符號模擬為基礎進行設計驗證的架構上，首先提出了符號偏序規約的技術來減少對等價的排程選擇的探索。除此之外，對於那些不能以偏序規約化簡的排程選擇，我們嘗試將這些排程選擇上的執行路徑(以及其相關的狀態)合併為較少的執行路徑以避免驗證引擎在執行路徑數量上的爆炸。實驗結果顯示，藉由結合這兩種技術，我們的驗證引擎在可擴展性上達到了巨大的提升。 | zh_TW |
| dc.description.abstract | Due to the non-determinism of the SystemC scheduler, formal SystemC verification must deal with a scalability issue. The issue stems from enumerating all scheduling alternatives such that all design behaviors can be captured assuredly. To conquer the scheduling alternative explosion problem under our symbolic simulation based verification scheme, we first adopt symbolic partial order reduction to reduce the equivalent scheduling alternatives for exploration. Moreover, for those scheduling alternatives that cannot be reduced by partial order reduction, we merge their execution paths (and also states) into fewer ones to prevent the number of paths from explosion. The experimental results show that we achieve a tremendous scalability improvement by combining these two techniques together. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-16T13:25:21Z (GMT). No. of bitstreams: 1 ntu-102-R00943083-1.pdf: 3595432 bytes, checksum: 7f346970326cf10a55f8db8d552830b0 (MD5) Previous issue date: 2013 | en |
| dc.description.tableofcontents | 口試委員會審定書 i
誌謝 ii 中文摘要 iii ABSTRACT iv CONTENTS v LIST OF FIGURES vii LIST OF TABLES viii Chapter 1 Introduction 1 1.1 Related Work 2 1.2 The Organization of This Thesis 5 Chapter 2 The Scheduling Alternative Explosion Problem of SystemC 6 2.1 The Basic SystemC Constructs 6 2.2 The SystemC Scheduler 9 2.3 The Scheduling Alternative Explosion Problem 11 Chapter 3 Our Framework 14 3.1 The Front-end Parser and Internal Representation 15 3.2 The Back-end Formal Engine 17 Chapter 4 Preliminaries 20 4.1 Partial Order Reduction 21 4.2 Symbolic Simulation 22 4.3 Formal Setting of SystemC 25 Chapter 5 Symbolic Partial Order Reduction for SystemC Symbolic Simulation 27 5.1 Constructing the Independence Relation 28 5.2 Dynamic Process Independence Relation Inference 29 5.3 Scheduling Exploration 30 Chapter 6 Merge Execution Paths with Scheduling Encoding 33 6.1 Merging Requirements 34 6.2 Scheduling Encoding 36 Chapter 7 Experiments 38 7.1 Case Analysis 38 7.2 More Benchmarks 40 Chapter 8 Conclusion 43 REFERENCE 44 | |
| dc.language.iso | en | |
| dc.title | 解決SystemC正規驗證中之排程選擇數量爆炸之問題 | zh_TW |
| dc.title | Conquering the Scheduling Alternative Explosion Problem of Formal SystemC Verification | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 101-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 蔡仁松(Ren-Song Tsay),洪士灝(Shih-Hao Hung),王柏堯(Bow-Yaw Wang) | |
| dc.subject.keyword | SystemC,正規驗證,排程選擇,偏序規約,符號模擬,合併執行路徑, | zh_TW |
| dc.subject.keyword | SystemC,formal verification,scheduling alternatives,partial order reduction,symbolic simulation,execution path merging, | en |
| dc.relation.page | 46 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2013-07-23 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
| 顯示於系所單位： | 電子工程學研究所 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-102-1.pdf 目前未授權公開取用 | 3.51 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。