指導教授：黃鐘揚臺灣大學：電子工程學研究所吳柏翰Wu, Bo-HanBo-HanWu2014-11-302018-07-102014-11-302018-07-102014http://ntur.lib.ntu.edu.tw//handle/246246/263899現今為了驗證某些系統性的性質，限制隨機驗證方法(CRV)逐漸成為主流。主要原因是CRV擁有更高的效率和更好的擴展性。在此驗證方法中，驗證工程師只須撰寫限制式來表達待驗證的環境，而不需繁瑣地描述每個模擬測試的數值。當撰寫完這些限制式後，可透過限制式求解器來求解這些限制式，產生滿足限制的測試數值，進而模擬整個電路。為了保證主要的驗證可以花費於模擬電路和確認觀測的性質對錯上，產生符合限制式之測試數值的過程只能耗費相對少量的計算資源。另一方面，為了保證最好的驗證品質，VDL標準要求產生的模擬數值分布必須要均勻或者是符合驗證工程師所設定的機率分布。 在此研究中，我們提出一個限制求解技術來加速模擬數值的產生過程。而此法我們簡稱為RSSDE技術。我們主要著重在克服以下三個挑戰：1) 產生模擬數值以及滿足機率分步的權衡 2) 驗證限制式中包含變數順序的條件 3) 驗證環境中包含多種限制式的不同組合。以上這些挑戰皆在業界驗證環境中時常出現，像是出現於UVM或VVM的驗證環境中。而我們提出的技術保證加速產生過程，且同時滿足驗證工程師所要求的模擬數值機率分布。實驗結果亦顯示，在與業界所開發的系統比較，我們所提出的技術擁有較高速率的模擬數值產生優勢。Nowadays, Constrained Random Verification (CRV) methodology is becoming the mainstream to verify system-wide properties for the advantage of its scalability and efficiency. Verification engineers implement verification scenario by writing constraints instead of explicitly specifying simulation patterns. A constraint solver is then applied to solve those constraints and generate feasible stimuli to exercise the design. To assure that the majority of the verification efforts are spent on the simulation of the design and the validation of the assertions/monitors, it is required that the pattern generation process should be computationally inexpensive and thus only consume a small fraction of the computing resource. On the other hand, to ensure the best verification quality, it is specified in the VDL manual that the distribution of the generated stimuli should be even or meet the user-specified distribution. In this dissertation, we propose a constrained pattern generation technique which is called “Range-Splitting and Solution-Density Estimation (RSSDE)” to accelerate the pattern generation processes. We focus on conquering three practical challenges: 1) the tradeoff between pattern generation speed and distribution requirement 2) testbench with solving-order constraints 3) testbench with multiple constraint sets. The above three issues frequently appear in real verification environment like UVM and VVM. Furthermore, we guarantee that the generated patterns satisfy the distribution requirement with the benefits of pattern generation acceleration. The experimental results demonstrate the robustness and efficiency of our framework when compared to a commercial tool.口試委員會審定書 i 誌謝 ii 中文摘要 iii ABSTRACT iv CONTENTS v LIST OF FIGURES ix LIST OF TABLES xv Chapter 1 Introduction 1 1.1 Problem Formulation 2 1.1.1 Variables 3 1.1.2 Constraints 4 1.2 Related Literature 5 1.3 Contribution 7 1.4 Organization of Dissertation 9 Chapter 2 Preliminaries 10 2.1 Constrained Random Verification (CRV) 10 2.2 Constraint Satisfaction Problem (CSP) 13 2.3 SAT and SMT Problems 15 Chapter 3 Backbone Algorithm - RSSDE Technique 17 3.1 Overview of the Proposed Framework 17 3.2 Range-Splitting Tree 19 3.3 Range-Splitting Heuristics 22 3.3.1 Bisection Points 24 3.3.2 Constraint-based Points 24 3.3.3 Split-on-Demand (SoD) Technique 25 3.4 Solution-Density Estimations Technique 25 3.5 The RSSDE Algorithm 28 3.6 RS-Tree Guided Pattern Generation 31 3.7 Pragmatic Issues of RS-Trees 33 3.7.1 RS-Tree Constructing Orders 33 3.7.2 Error Accumulation on RS-Trees 34 3.7.3 Low-Solution-Density Nodes 34 Chapter 4 Generalized RSSDE Technique for Arbitrary Distribution 37 4.1 Definitions 38 4.2 Generalized Range-Splitting Tree 40 Chapter 5 Extension to Handle Variable-Ordering Constraints 46 5.1 Introduction 46 5.2 Problem Formulation of Variable-Ordering Constraints 49 5.3 An Exhaustive Solution 51 5.4 Flow of our Framework 51 5.5 Data Structure: Range-Feasibility Tree 54 5.6 Construction of Range-feasibility Trees 56 5.7 Range Reduction Technique on Range-feasibility Trees 58 5.8 Solution Space Profiles in Different Projection Directions 62 5.9 A Running Example 66 5.10 Conditional Evenness Ensurance 68 Chapter 6 Extension to Handle Multiple Constraint Sets 70 6.1 Problem Formulation 71 6.2 Flow to Handle Multiple Constraint Sets 72 6.3 Incremental RS-Tree Construction Technique under Multiple Constraint Sets 74 6.3.1 Incremental RS-Tree Construction for Relaxation 75 6.3.2 Incremental RS-Tree Construction for Restriction 77 6.4 Pseudocode of our Incremental Construction Algorithm 81 6.5 Constrained Pattern Generation Procedure 82 Chapter 7 Evaluation of Pattern Generation Throughput and Distribution Evenness 84 7.1 Throughput Evaluation 84 7.2 Evenness Evaluation 84 7.2.1 Distance of the Nearest Point 84 7.2.2 K-Means Clustering Analysis 85 7.3 User-Specified Distribution Evaluation 87 Chapter 8 Experimental Results 89 8.1 Testbench for General Distribution 89 8.1.1 Speed Analysis for Evenness Distribution Cases 89 8.1.2 Distribution Analysis for Evenness Distribution Cases 91 8.1.3 Speed Analysis for User-specified Distribution Cases 94 8.1.4 Distribution Analysis for User-specified Distribution Cases 94 8.1.5 Analysis of RS-Tree Construction Time 96 8.2 Testbench with Variable-Ordering Constraints 98 8.2.1 Analysis of Pattern Generation Speed 98 8.2.2 Number of Orders Versus Runtime 101 8.2.3 Comparison Details of Different Techniques 101 8.3 Testbench with Multiple Constraint Sets 104 8.3.1 Analysis of Pattern Generation Speed 104 8.3.2 Speed Comparison on Various Techniques 104 8.3.3 Analysis of RS-Tree Construction Time 107 8.4 Limitations and Future Works 108 Chapter 9 Conclusions 110 REFERENCES 1122079877 bytesapplication/pdf論文公開時間：2015/09/03論文使用權限：同意有償授權(權利金給回饋學校)功能性驗證CRVSystemVerilog樣式分布限制求解thesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/263899/1/ntu-103-D99943038-1.pdf