指導教授：黃鐘揚臺灣大學：電子工程學研究所吳政穎Wu, Cheng-YinCheng-YinWu2014-11-302018-07-102014-11-302018-07-102014http://ntur.lib.ntu.edu.tw//handle/246246/263953模型檢驗（亦稱為屬性檢驗）是一種典型的方法用以正規地驗證一個硬體系 統。給定一個硬體系統與一組屬性，模型檢驗演算法將斷定該系統滿足以及不滿 足哪些屬性。然而隨著設計複雜度不斷地提高以及所需檢驗的屬性數量隨之增 加，模型檢驗的能力將因其本身的高複雜度而下降。 在這篇博士論文中我們發表了一個工具適用於暫存器轉移階層硬體系統的模 型檢驗。該工具包含了以下三個部分：正規模型、前端處理、以及模型檢驗。首 先正規模型將對一個複雜的暫存器轉移階層硬體系統進行解析與合成，最後將它 表示成一個文字階層的電路。其次，在前端處理中我們將該電路進行改寫以及重 新合成，並進一步從該電路的抽象層面抽取與所需檢驗之屬性相關的條件與恆真 屬性，以促進模型檢驗。在前端處理最後所需驗證之屬性都將被合成之後。在模 型檢驗階段，我們設計了一個組合式的模型檢驗器用以檢驗所有的屬性。特別的 是，各式各樣的屬性檢驗演算法將在第一時間互相分享彼此獲得的情報（例如： 已知最深的臨界，以及計算出可達到之範圍等等），以彌補單一演算法能力之不 足。我們採用了數個暫存器轉移階層的驗證問題作為實驗的對象，而實驗結果說 明了我們所提出的技術讓我們的驗證工具能夠有效地處理包含數千個屬性的複雜 模型檢驗問題。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.1 Introduction 1 2 Preliminaries 8 2.1 Register Transfer Level (RT-Level) Hardware Description Language . . . 8 2.2 Word-level Network . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.3 Propositional Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.4 Transition System of a Network . . . . . . . . . . . . . . . . . . . . . . 12 2.5 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.5.1 Property Specification . . . . . . . . . . . . . . . . . . . . . . . 13 2.5.2 Safety Property Checking . . . . . . . . . . . . . . . . . . . . . 15 2.5.3 Liveness Property Checking . . . . . . . . . . . . . . . . . . . . 18 2.6 Abstract Transition System . . . . . . . . . . . . . . . . . . . . . . . . . 20 3 Formal Modeling of RT-level Hardware Systems 22 3.1 Front-end Modeling of RT-Level Hardware Systems . . . . . . . . . . . . 23 3.2 The Construction of a Word-level Network for Verification . . . . . . . . 25 3.2.1 Signals and Flip-Flops of a Network . . . . . . . . . . . . . . . . 26 3.2.2 Operators in a Network . . . . . . . . . . . . . . . . . . . . . . . 26 3.2.3 Representation of a Network . . . . . . . . . . . . . . . . . . . . 28 3.2.4 The Construction of Word-level Networks from QuteRTL . . . . 30 3.3 Property Elaboration . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.3.1 Addressing Invariant Constraints . . . . . . . . . . . . . . . . . . 32 3.3.2 Liveness Checking as Safety Checking . . . . . . . . . . . . . . 34 3.4 Optimizing the Elaborated Network . . . . . . . . . . . . . . . . . . . . 37 3.4.1 Cone-of-Influence Reduction . . . . . . . . . . . . . . . . . . . . 38 3.4.2 Structural Hashing . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.4.3 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.4.4 Bit-Blasting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4 Preprocessing Techniques Toward Verification Instance Optimization 42 4.1 Extracting Property-directed Invariant for Safety Properties . . . . . . . . 43 4.1.1 Combinational and Sequential Invariants . . . . . . . . . . . . . 43 4.1.2 The Construction of Abstract Transition Systems . . . . . . . . . 45 4.1.3 Extracting Invariants from Abstract Transition Systems . . . . . . 56 4.2 Extracting Fairness Constraints for Liveness Properties . . . . . . . . . . 58 5 A Portfolio-based Model Checker for Checking Single Property 61 5.1 Hardware Model Checking: Trends and Facts . . . . . . . . . . . . . . . 62 5.1.1 Problem Formulation to a Single Property Checking Instance . . . 63 5.1.2 Existing Approaches to Single Property Checking . . . . . . . . . 64 5.2 Towards an Efficient Portfolio-based Model Checker for Single Property Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 5.2.1 An Overview of Our Portfolio-based Model Checker . . . . . . . 67 5.2.2 Model Checking Algorithms: Comparisons, Analyses, and Summaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.2.3 Model Checking Cloud: A Platform for Information Sharing . . . 73 5.2.4 The Resource Control Mechanism . . . . . . . . . . . . . . . . . 76 6 A Portfolio-based Model Checker for Checking Multiple Properties 81 6.1 The Differences between Checking Multiple Properties and Single Property 82 6.1.1 A Summary to The Multiple Property Track of HWMCC . . . . . 82 6.1.2 Practical Issues to Model Checking Multiple Properties . . . . . . 84 6.2 Towards a High-throughput Portfolio-based Model Checker for Multiple Property Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 6.2.1 Property Reordering . . . . . . . . . . . . . . . . . . . . . . . . 88 6.2.2 Model Checking Cloud Revisited . . . . . . . . . . . . . . . . . 93 6.2.3 More on the Resource Control Mechanism . . . . . . . . . . . . 95 6.3 Incremental Model Checking: Never Start-over . . . . . . . . . . . . . . 98 6.3.1 Making a Model Checking Procedure Incremental . . . . . . . . 99 6.3.2 Rendering a Model Checking Algorithm Incremental . . . . . . . 100 7 Experimental Evaluation 106 7.1 Experimental Evaluation of Formal Modeling . . . . . . . . . . . . . . . 108 7.2 Experimental Evaluation of Preprocessing . . . . . . . . . . . . . . . . . 112 7.2.1 The Effect of Property-directed Invariants to Safety Checking . . 113 7.2.2 The Effect of Fairness Constraints to Liveness Checking . . . . . 117 7.3 Experimental Evaluation of Single Property Checking . . . . . . . . . . . 120 7.3.1 Effect of Shared Information to Runtime Performance . . . . . . 121 7.3.2 Effect of Shared Information to Deep Bound . . . . . . . . . . . 124 7.4 Experimental Evaluation of Multiple Property Checking . . . . . . . . . 125 7.4.1 A Toolbox for Property Generation . . . . . . . . . . . . . . . . 125 7.4.2 The Result of Multiple Property Checking . . . . . . . . . . . . . 130 8 Conclusions and Future Work 135 References 1386025400 bytesapplication/pdf論文公開時間：2014/08/21論文使用權限：同意無償授權正規驗證硬體模型檢驗thesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/263953/1/ntu-103-D99943034-1.pdf