利用延伸斐氏網路模型實現之SystemC設計死鎖狀態檢查技術

Abstract

由於SystemC是一個越來越普遍用來處理日益複雜的現代系統層級設計的塑模語言，在SystemC 設計上進行快速，準確地模擬，和執行牢靠的功能驗證的工具已成為整個設計流程中最重要的部分。由於傳統的編譯代碼模擬器是將一個SystemC設計編譯到低階可執行程式，它們只能進行模擬驗證。因此，當設計存在不單純的錯誤，例如死鎖情況，幾乎是不可能的去進一步分析設計的功能性以找出錯誤原因。 在此論文中，我們針對SystemC設計提出了一個延伸斐氏網路模型。此外，基於這個模型，我們還實作了一個SystemC的模擬器。由於擁有一個SystemC設計的內部表示以及對於模擬時排程的控制性，我們將可以對SystemC設計進行死鎖檢查。我們提出的演算法首先分析了SystemC設計中並行程序彼此之間事件同步的相依性。同時，我們將此相依性透過一個圖形化的資料結構呈現給設計者，以幫助他們瞭解死鎖產生的原因。透過幾個有效的例子，我們將證明所提出的模型和死鎖檢查的正確性。 此外，我們所提出的延伸斐氏網路模型也可以作為SystemC設計的正規表示。這為未來對於應用正規驗證技術於SystemC設計上的研究開創相當大的可能性。

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