應用於系統單晶片中介面相符驗證之正規方法

Abstract

在系統單晶片的整合過程中，驗證所要整合到系統中的區塊是否符合其介面協定，乃是一不可忽略之重要步驟。然而，現存的幾種方法各有其實用上之限制：以模擬為基礎的方法常常忽略了沒有被模擬到的情況而發生錯誤，而正規方法容易遭遇記憶體不足及執行時間過長的問題。此論文為此種介面協定之相符驗證提出一新穎的演算法。此法乃是將介面協定之特性表示成一有限狀態機，然後在較電路層級更高的有限狀態機層級，以正規方法來驗證介面的邏輯。相較於以其他特性規格語言來表示介面協定之特性，有限狀態機的表示法更為系統化，這大大地降低了特性表示不完全的可能性。此外，理論推算及實驗結果都顯示此演算法能在合理的時間及記憶體需求內完成驗證。

Verifying whether a building block conforms to certain interface protocol is one of the important steps while constructing a system-on-a-chip (SoC). However, most existing methods have their own limitations. Simulation-based methods have the false positive problem while formal property checking methods may suffer from memory explosion and excessive runtime. In this thesis, we propose a novel branch-and-bound algorithm for interface protocol compliance verification. The properties of the interface protocol are specified as a specification FSM, and the interface logic is formally verified at the higher FSM level. Using the FSM for property specification is relatively systematic than using other proprietary property languages, which greatly reduces the possibility of incomplete property identification. And it is shown theoretically and experimentally that the proposed algorithm can finish in reasonable time and space complexity.