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/43823
完整後設資料紀錄
DC 欄位值語言
dc.contributor.advisor黃鐘揚
dc.contributor.authorSiao-Jie Caien
dc.contributor.author蔡曉傑zh_TW
dc.date.accessioned2021-06-15T02:29:41Z-
dc.date.available2009-08-18
dc.date.copyright2009-08-18
dc.date.issued2009
dc.date.submitted2009-08-15
dc.identifier.citation[1] M.He, M.C. Tsai, X. Wu, F. Wang, and R. Nasr, “Hardware/Software Codesign Pedagogy for the Industry,” in Proceedings of Fifth International Conference on Information Technology: New Generations, 2008, pp. 279-284.
[2] Open SystemC Initiative. http://www.systemc.org/
[3] SpecC. http://www.cecs.uci.edu/~specc/
[4] Arvind, “Bluespec: A language for hardware design, simulation, synthesis and verification Invited Talk,” in Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-Design, IEEE Computer Society, 2003, p. 249.
[5] M.Y. Vardi, “Formal techniques for SystemC verification,” in Proceedings of the 44th annual Design Automation Conference, San Diego, California: ACM, 2007, pp. 188-192.
[6] J. L. Peterson, Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981.
[7] C. Girault, R. Valk, Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications. New York: Springer, 2002,
[8] D. Karlsson, P. Eles, and Z. Peng, “Formal verification of SystemC designs using a Petri-net based representation,”in Proceedings of the conference on Design, automation and test in Europe, 2006, pp. 1228-1233.
[9] A. Sen, V. Ogale, and M.S. Abadir, “Predictive runtime verification of multi-processor SoCs in SystemC,”in Proceedings of the 45th annual Design Automation Conference, Anaheim, California: ACM, 2008, pp. 948-953.
73
[10] E. Cheung, P. Satapathy, Vi Pham, H. Hsieh, and Xi Chen, “Runtime Deadlock Analysis of SystemC Designs,”in Proceedings of the IEEE International High-Level Design Validation and Test Workshop (HLDVT). Eleventh Annual IEEE International, 2006, pp. 187-194.
[11] T. Groetker, S. Liao, G. Martin, and S. Swan. System Design with SystemC. Norwell, MA, Kluwer Academic Publishers, 2002.
[12] D.C. Black, J. Donovan, SystemC from the Ground Up. Norwell, MA, Kluwer Academic Publishers, 2004.
[13] J. Ruf, D. Hoffmann, J. Gerlach, T. Kropf, W. Rosenstiehl, and W. Mueller, “The simulation semantics of systemC,”in Proceedings of the conference on Design, automation and test in Europe, Munich, Germany: IEEE Press, 2001, pp. 64-70.
[14] X. Chen, A. Davare, H. Hsieh, A. Sangiovanni-Vincentelli, and Y. Watanabe,“Simulation based deadlock analysis for system level designs,”in Proceedings of the 42nd annual conference on Design automation, Anaheim, California, USA: ACM, 2005, pp. 260-265.
dc.identifier.urihttp://tdr.lib.ntu.edu.tw/jspui/handle/123456789/43823-
dc.description.abstract由於SystemC是一個越來越普遍用來處理日益複雜的現代系統層級設計的塑模語言,在SystemC 設計上進行快速,準確地模擬,和執行牢靠的功能驗證的工具已成為整個設計流程中最重要的部分。由於傳統的編譯代碼模擬器是將一個SystemC設計編譯到低階可執行程式,它們只能進行模擬驗證。因此,當設計存在不單純的錯誤,例如死鎖情況,幾乎是不可能的去進一步分析設計的功能性以找出錯誤原因。
在此論文中,我們針對SystemC設計提出了一個延伸斐氏網路模型。此外,基於這個模型,我們還實作了一個SystemC的模擬器。由於擁有一個SystemC設計的內部表示以及對於模擬時排程的控制性,我們將可以對SystemC設計進行死鎖檢查。我們提出的演算法首先分析了SystemC設計中並行程序彼此之間事件同步的相依性。同時,我們將此相依性透過一個圖形化的資料結構呈現給設計者,以幫助他們瞭解死鎖產生的原因。透過幾個有效的例子,我們將證明所提出的模型和死鎖檢查的正確性。
此外,我們所提出的延伸斐氏網路模型也可以作為SystemC設計的正規表示。這為未來對於應用正規驗證技術於SystemC設計上的研究開創相當大的可能性。
zh_TW
dc.description.abstractAs SystemC is becoming the prevailing modeling language to handle the increasing complexity of the modern system-level designs, tools to conduct fast and accurate simulation and perform solid functional verification on SystemC designs have become the most critical component in the design flow. Since conventional compiled code simulators compile the SystemC designs into low-level executable programs, they can only perform simulation-based validation. Therefore, it is virtually impossible to further analyze the design functionality for the non-trivial design errors such as dead-lock condition.
In this thesis, we proposed an extended Petri-Net model for SystemC designs. We also implemented a SystemC simulator based on this model. With the internal representation of the SystemC designs and the controllability on the simulation scheduling, we are able to perform the deadlock checks of the SystemC designs. Our proposed algorithm first analyzes the dependencies of the event synchronization for the concurrent processes in the SystemC design. And a graph data structure is then presented to help designers to figure out the causes of the deadlock. We will demonstrate the correctness of the proposed model and the deadlock checking through several working examples.
Furthermore, the proposed extended Petri-Net model can also act as a formal representation of a SystemC design. This brings up a lot of possibilities for the research with formal verification techniques in the future.
en
dc.description.provenanceMade available in DSpace on 2021-06-15T02:29:41Z (GMT). No. of bitstreams: 1
ntu-98-R96921034-1.pdf: 1199986 bytes, checksum: 617295b8a81dd412368437da1c335f94 (MD5)
Previous issue date: 2009
en
dc.description.tableofcontents口試委員會審定書 #
誌謝 i
摘要 ii
ABSTRACT iii
TABLE OF CONTENTS iv
LIST OF FIGURES vii
LIST OF TABLES ix
LIST OF ALGORITHMS x
Chapter 1 Introduction 1
1.1 Introduction to Electronic System Level Designs 1
1.2 Objectives of the Thesis 2
1.3 Previous Works 3
1.4 Organization of the Thesis 3
Chapter 2 Preliminaries 5
2.1 SystemC Overview 5
2.1.1 SystemC Components 5
2.1.2 SystemC Simulation Kernel 8
2.2 Event in SystemC 10
2.2.1 Static and Dynamic Sensitivity 10
2.2.2 Event Notification 12
2.3 Deadlock in SystemC 12
2.4 Basic Concepts of Petri Net 14
2.4.1 Basic Definitions 15
2.4.2 Executions Rules 17
Chapter 3 Proposed Extended Petri Net Model of SystemC Designs 20
3.1 Review of the Previous Extended Petri Net Model 20
3.2 Proposed Extended Petri Net Model 20
3.3 Modeling of C++ Construct 22
3.3.1 Variables 23
3.3.2 Expressions Statements 23
3.3.3 Conditional Expressions 26
3.3.4 Control Flow Statements 27
3.4 Modeling of SystemC Construct 29
3.4.1 Process 29
3.4.2 Port and Signal 30
3.4.3 Wait Statement 32
3.4.4 Event Notification 34
Chapter 4 SystemC Simulation Using Proposed Extended Petri Net Model 36
4. Overview of the Extended Petri Net SystemC Scheduler 36
4.2 Simulation Algorithm for Extended Petri Net Model 37
4.3 SystemC Simulation Kernel on Extended Petri Net Model 37
4.3.1 Initialization Phase 38
4.3.2 Evaluation Phase 38
4.3.3 Update Phase 39
4.3.4 Time Notification Phase 39
Chapter 5 Petri Net Based Static Property Checker 40
5.1 Overview of Static Property Checker on Petri Net Model 40
5.2 Dynamic Synchronization Dependency Graph 41
5.3 Proposed Predictive Synchronization Dependency Graph 42
5.4 Modeling of Deadlock Checking 45
5.5 Structural Checking of PSDG 47
5.6 Simulation Based Deadlock Checking 53
5.6.1 Heuristic Watch Criteria 55
5.7 Comparison with Previous Works 57
Chapter 6 Experimental Results 59
6.1 Test Cases Description 59
6.2 SystemC to Extended Petri Net Translation 60
6.3 Deadlock Checking 64
6.4 Profiling Result of Execution Time 67
6.5 Comparision with OSCI SystemC Simulator 68
Chapter 7 Conclusion and Future Work 70
REFERENCE 72
dc.language.isoen
dc.subject模擬確認zh_TW
dc.subjectSystemCzh_TW
dc.subject死鎖zh_TW
dc.subject電子系統層級zh_TW
dc.subjectelectronic system levelen
dc.subjectSystemCen
dc.subjectdeadlocken
dc.subjectsimulation validationen
dc.title利用延伸斐氏網路模型實現之SystemC設計死鎖狀態檢查技術zh_TW
dc.titleDeadlock Checking of SystemC Designs Using Extended Petri-Net Modelen
dc.typeThesis
dc.date.schoolyear97-2
dc.description.degree碩士
dc.contributor.oralexamcommittee王凡,洪士灝,茅華
dc.subject.keywordSystemC,死鎖,模擬確認,電子系統層級,zh_TW
dc.subject.keywordSystemC,deadlock,simulation validation,electronic system level,en
dc.relation.page73
dc.rights.note有償授權
dc.date.accepted2009-08-17
dc.contributor.author-college電機資訊學院zh_TW
dc.contributor.author-dept電機工程學研究所zh_TW
顯示於系所單位:電機工程學系

文件中的檔案:
檔案 大小格式 
ntu-98-1.pdf
  未授權公開取用
1.17 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