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

Abstract

現今在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.