利用性質導向可達度技術進行正規SystemC設計驗證

Formal SystemC Verification based on Property-Directed Reachability

王冠璋(Kuan-Chang Wang)

指導教授 ： 黃鐘揚

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2012年)

https://doi.org/10.6342/NTU.2012.03345

摘要

現今在System-on Chip的許多模組是以高階語言所描述完成, 然而在高階語言中, SystemC以它高效能的速度脫穎而出, 成為業界所認定的標準高階語言, 也因為如此, 在IC晶片設計流程中, SystemC 的設計驗證是非常重要且關鍵.
在這篇論文中, 我們以正規方法定義狀態變數並且以完全符號化模擬建立出變換聯繫, 在我們的正規模組之下, 我們能夠較容易地去實現其他軟硬體上的技術, 並且考慮SystemC上各個角度下的許多語意. 另一方面, 我們也運用無邊際模組檢驗的演算法去驗證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.

並列關鍵字

SystemC ； formal SystemC verification ； formal model ； fully symbolic simulation ； Property-Directed Reachability

參考文獻

[3] B. Bailey, G. Martin and A. Piziali, ESL Design and Verification: A Prescription for Electronic System Level Methodology. Morgan Kaufmann/Elsevier. 2007

[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.