請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/61717
標題: | 利用性質導向可達度技術進行正規SystemC設計驗證 Formal SystemC Verification based on Property-Directed Reachability |
作者: | Kuan-Chang Wang 王冠璋 |
指導教授: | 黃鐘揚(Chung-Yang (Ric) |
關鍵字: | SystemC,正規SystemC 驗證,正規模組,完全符號化模擬,性質導向可達度技術, SystemC,formal SystemC verification,formal model,fully symbolic simulation,Property-Directed Reachability, |
出版年 : | 2012 |
學位: | 碩士 |
摘要: | 現今在System-on Chip的許多模組是以高階語言所描述完成, 然而在高階語言中, SystemC以它高效能的速度脫穎而出, 成為業界所認定的標準高階語言, 也因為如此, 在IC晶片設計流程中, SystemC 的設計驗證是非常重要且關鍵.
在這篇論文中, 我們以正規方法定義狀態變數並且以完全符號化模擬建立出變換聯繫, 在我們的正規模組之下, 我們能夠較容易地去實現其他軟硬體上的技術, 並且考慮SystemC上各個角度下的許多語意. 另一方面, 我們也運用無邊際模組檢驗的演算法去驗證SystemC的設計, 然而我們在要將這個演算法轉換到高階語言中遇到許多挑戰, 因此我們也提出許多技術去克服這些困難, 最後, 實驗數據顯示出我們演算法的效能和能夠掌握的設計大小. 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. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/61717 |
全文授權: | 有償授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-101-1.pdf 目前未授權公開取用 | 3.62 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。