暫存器轉移階層硬體系統模型檢驗

Abstract

模型檢驗（亦稱為屬性檢驗）是一種典型的方法用以正規地驗證一個硬體系 統。給定一個硬體系統與一組屬性，模型檢驗演算法將斷定該系統滿足以及不滿 足哪些屬性。然而隨著設計複雜度不斷地提高以及所需檢驗的屬性數量隨之增 加，模型檢驗的能力將因其本身的高複雜度而下降。 在這篇博士論文中我們發表了一個工具適用於暫存器轉移階層硬體系統的模 型檢驗。該工具包含了以下三個部分：正規模型、前端處理、以及模型檢驗。首 先正規模型將對一個複雜的暫存器轉移階層硬體系統進行解析與合成，最後將它 表示成一個文字階層的電路。其次，在前端處理中我們將該電路進行改寫以及重 新合成，並進一步從該電路的抽象層面抽取與所需檢驗之屬性相關的條件與恆真 屬性，以促進模型檢驗。在前端處理最後所需驗證之屬性都將被合成之後。在模 型檢驗階段，我們設計了一個組合式的模型檢驗器用以檢驗所有的屬性。特別的 是，各式各樣的屬性檢驗演算法將在第一時間互相分享彼此獲得的情報（例如： 已知最深的臨界，以及計算出可達到之範圍等等），以彌補單一演算法能力之不 足。我們採用了數個暫存器轉移階層的驗證問題作為實驗的對象，而實驗結果說 明了我們所提出的技術讓我們的驗證工具能夠有效地處理包含數千個屬性的複雜 模型檢驗問題。

Model checking, or property checking, is a classic methodology for formally verifying a hardware system. More specifically, given a system and a set of properties, model checkers judge whether the system satisfies a property or not. However, due to the high complexity of model checking, as the design complexity and the number of property to be verified grows rapidly, the capability of model checking decreases. In this thesis, we present a complete framework for model checking of RT-level hardware systems. The framework consists of three major building blocks: FORMAL MODELING, PREPROCESSING, and MODEL CHECKING. Starting from FORMAL MODELING, a complicated RT-level design is parsed, synthesized, and then modeled as a word-level network. Next in the PREPROCESSING stage, rewriting and resynthesis techniques are applied to optimize the network, and moreover, property-directed constraints and invariants are extracted from design abstraction for improving model checking. After properties are elaborated at the end of PREPROCESSING, a portfolio-based model checker starts to verify all the properties in the MODEL CHECKING stage, and in particular, different model checking algorithms share information (e.g. deep bounds and reachabilities) on-the-fly to complement each other. Our experimental evaluation shows that our framework, equipped with abovementioned techniques, is capable of model checking RT-level benchmarks with thousands of properties efficiently.