朝向SystemC設計之正規驗證

Abstract

在所有系統層級的描述語言中，SystemC成為描述複雜電子系統上，一個開放原始碼的工業標準。在早期電子系統設計的過程當中，驗證SystemC的設計是至關重要的，因為它能夠避免設計的錯誤發生在最後的實現上。然而到目前為止，SystemC的驗證主要還是依賴傳統的動態驗證技術。另一方面，傳統硬體的正規驗證方法，無法容易地應用於SystemC的驗證，主要是因為傳統硬體的正規驗證方法，靠著是將設計轉換為邏輯電路，但是從SystemC的設計合成到邏輯電路之間的選擇實在是太多，造成採用傳統硬體的正規驗證方法上的困難。近幾年來，有一些研究團隊試圖將軟體的正規驗證方法擴展到SystemC的設計之上。然而，這些研究要不抽象化了SystemC 調度器的相關語意，或者顯示有限的可擴展性。 因此，作為朝向SystemC設計之正規驗證，我們開發了一個正規驗證架構，用來檢查SystemC設計上的鎖死狀態。就理論的層面上，我們提出了符號模型檢查技術來正規地驗證SystemC的設計，在我們所提出的符號模型檢查中，我們利用了有界模型檢查和歸納法的概念。為了保證我們所提出方法的正確性，我們引進行為狀態和行為轉變這兩個觀念。就實作的層面上，我們提出了三層的模型來表示SystemC的設計。透過使用不同的結構，我們的模型可以忠實地且簡潔地捕捉原有設計的語意。此外，我們又提出了一個有效的符號模擬器，此符號模擬器除了作用於我們所提出的三層模型之外，它也會產生正規證明供符號模型檢查使用。藉由各種新穎的構想，實驗結果顯示我們在SystemC設計之上的正規鎖死檢查是非常可靠且有效的。

Among all the system-level description languages, SystemC emerges as an open and industry standard for complex electronic systems. In the early design stage of electronic systems, verifying SystemC designs is crucial since it can avoid propagating design errors down to the final implementation. However, the traditional dynamic validation techniques have been the main workhorses of the SystemC verification until now. On the other hand, traditional formal verification techniques for hardware, which rely on the translation of designs under verification into logic netlists, cannot be easily adopted here due to the abundant synthesis flexibilities of SystemC designs. Recently, some works have tried to extend formal verification techniques for software to SystemC designs. Nevertheless, they abstract away relevant semantic aspects of the SystemC scheduler or show limited scalability. Therefore, as an innovative step toward formal verification on SystemC designs, we develop a formal verification framework for the deadlock checking on SystemC designs. For the theoretical aspect of our formal verification framework, we devise a symbolic model checking approach using bounded model checking and inductive step to formally verify the properties in SystemC designs. In order to guarantee the soundness of our approach, we introduce the notions of behavioral states and behavioral transitions. Besides, we present an encoding mechanism to make our symbolic model checking approach on SystemC designs more scalable and effective. For the pragmatic aspect of our framework, we propose a multi-layer modeling to represent SystemC designs. By using three distinct but still interrelated views to describe the semantics of high-level SystemC designs, our modeling can be very concise and faithfully capture the original design semantics. In addition, we implement an effective symbolic SystemC simulator which works on our multi-layer modeling and generates the formal proof for our symbolic model checking. With various novel ideas, our experimental results demonstrate the robustness and effectiveness of the formal deadlock checking on SystemC designs.