派屈網輔助邏輯電路模型檢查技術之研究

Abstract

隨著半導體製程的進步和電路系統設計的複雜度不斷增加，驗證這樣的系統以確保此設計正確無誤變成了一項困難的任務。要在這樣大又複雜的設計中找出問題變成了一項耗時卻又不可忽略的一個步驟。一般最常使用的驗證方法就是以模擬(simulation)的方式，設計者輸入適當的測試訊號，接著觀察輸出訊號是否正確來判斷設計的正確與否。這樣的驗證方式無法確保整個設計已經完全符合當初設計的規格沒有任何錯誤。Clarke和Allen Emerson發明了邏輯電路模型檢查(Model checking)技術，彌補了以模擬來驗證的不足之處。在這篇論文中，我們提出了一種以派屈網(Petri Net)輔助SMV model checker做邏輯電路模型檢查。利用派屈網的一些特性，加速對於運算樹狀邏輯(Computational tree logic, CTL)中的EF和EX類的特性(properties)的驗證速度。我們以C++實現了一個簡單的程式將有限狀態機(Finite state machine)轉換成派屈網並對其做驗證。在這篇論文中，我們展示了一些簡單的範例，比較PNV (Petri net verification)與SMV的驗證時間。我們下了一個結論:在部份情況下，PNV可以大幅降低驗證EF及EX所花費的時間。

With the progress of semiconductor manufacturing techniques and the increasing of complexity of designs, to ensure the correctness of a design becomes a hard mission. To find out the bugs in a large and complex design is time consuming but significant works. The general verification method used by designers is simulation. The designers input appropriate signals to the design and observe if the outputs are correct to judge the correctness of the design. This verification method can not ensure that the design is completely conform to the specification. Clarke and Allen Emerson invented model checking techniques to recover the insufficiency of simulation based verification. In this paper, we propose a Petri net-aided model checking techniques to assist SMV model checker. In some cases, this technique can speed up the verification of EF and EX properties. We implement a simple program with C++ language to transfer a FSM (finite state machine) into a Petri net and verify the state machine. Then we show some examples to compare the verification time of PNV and SMV. Finally we make a conclusion that in some cases, PNV can reduce the verification time of EF and EX properties substantially.