跳到主要內容

臺灣博碩士論文加值系統

(3.235.56.11) 您好!臺灣時間:2021/08/04 07:06
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:林恩祥
研究生(外文):En-Hsiang Lin
論文名稱:利用強健的全域與區域之無解空間辨識技術來提升限制性隨機樣本產生效能
論文名稱(外文):Improving Constrained Random Pattern Generation by Powerful Global and Local Infeasible Solution Space Identification
指導教授:黃鐘揚
指導教授(外文):Chung-Yang Huang
口試委員:李建模吳柏翰
口試委員(外文):Chien-Mo LiBo-Han Wu
口試日期:2015-07-28
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:電機工程學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2015
畢業學年度:103
語文別:英文
論文頁數:67
中文關鍵詞:功能性測試限制式隨機驗證範圍切割樹
外文關鍵詞:Functional VerificationConstrained Random VerificationRange Splitting Tree
相關次數:
  • 被引用被引用:0
  • 點閱點閱:67
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
功能性驗證在晶片設計流程上是不可或缺的一環。其中,直接測試是工業上最被廣泛使用的方法。它能在驗證初期快速檢驗電路基本功能。然而,其所產生的測試向量容易受限於使用者對待測系統的認知而產生分布不均的現象,使得一些角落錯誤不易觸發,進而影響到待測電路的測試覆蓋率。另一類被稱為限制式随機驗證的方法在近年來受到了重視。使用者只需根據待測電路規格與驗證的目標撰寫輸入限制式。接著,限制式求解器會自動產生大量滿足輸入限制式的測試向量。與直接測試的方法相比,它能快速並有效的產生更多的測試向量來模擬待測電路。
限制式求解技術是整個隨機驗證方法的核心。一個好的限制式求解器應該包含以下性質:1) 高生產率 2) 均勻分布(機率上) 3) 均勻分布(空間上)。換言之,它應該要能有效率的快速產生測試向量,並且同時保證產生的測試向量在機率和解空間角度上是均勻分散的。本篇論文針對一些較為困難的例子去提高測試向量的產生速率。我們的改進主是要建立在辨識更多的無解空間。當無解空間能辨識愈多,限制式求解器效率也會進一步提高。
我們把辨識流程分為兩階段:1) 全域無解空間辨識 2) 區域無解空間辨識。 兩者適用在不同的情況。在全域無解空間辨識的階段中,它過濾了包含有可全域式縮減變數的無解空間。一個變數如果初始範圍可以在不考慮其他變數的賦值下進行縮減,該變數稱為可全域式縮減變數。我們提出了一個迭代事件驅動的方法搭配正規詞級解法器去辨識出該類型變數。在區域無解空間辨識的階段,剩下的無解空間大部份是由可條件式縮減的變數所組成。一個變數如果需在同時考慮部份其他變數的數值情況下才能進行縮減,稱為可條件式縮減變數。我們使用了既有文獻裡所提出的範圍切割樹方法來過濾該類型的無解空間。範圍切割樹的樣式顯著地影響了無解空間辨識的能力。我們建置範圍切割樹的方法是去動態地選擇當下最困難的一條限制式做切割。實驗結果顯示,這種以貪心為基礎的建置方法能更有效地辨識出無解空間因此測試向量的生產率能因此大幅提高。


Functional verification is indispensable in circuit design flow. Directed testing is the most prevalently used method in industry. It can quickly validate basic functionality of design under verification (DUV) at the early stage. However, the generated test vectors are easily biased due to the designers’ perception on the DUV, which lowers the chance to trigger corner bugs. This greatly affects the test coverage of DUV. Another approach called Constraint Random Verification (CRV) draws more attention in recent years. Users provide input constraints based on system specification and their intention for verification, and then a constraint solver would efficiently generate vast amounts of patterns that satisfy the constraints. Compared to former approach, it can quickly generate more effective patterns to simulate the DUV.
Constraint solving technique is the key of CRV methodology. A good constraint solver for CRV should have the following properties: 1) high throughput 2) uniform distribution (in probability) 3) high pattern diversity (in search space). In other words, it should efficiently generate valid patterns while ensuring evenness and pattern diversity at the same time. In this thesis, we focus on improving throughput for some rather difficult cases. Our improvements mainly come from the identification of infeasible solution space for the input constraints. Intuitively, as more infeasible solution space is identified, the higher throughput the constraint solver can be achieved.
We divide the identification into two stages: 1) global infeasible space identification 2) local infeasible space identification. They apply to different situations. At global infeasible space identification stage, it filters out infeasible space which consists of universally reducible variables. A variable is universally reducible if its initial range can be reduced without consideration of the assignments of other variables. We proposed an iterative event-driven approach combined with the word-level SMT solver to identify such space. At local infeasible space identification stage, remaining infeasible space is mostly composed of conditionally reducible variables. A variable is conditionally reducible if its range can only be reduced with regard to the assignments of some of other variables. We utilize the Range Splitting Tree (RST) technique to filter out such infeasible space. The structure of constructed RST greatly affects the ability of infeasible space identification. Our RST construction is guided by dynamically selecting the constraint with lowest hit rate on-the-fly. Experimental results show the effectiveness of this greedy based construction to identify infeasible space, and thus the throughput can be substantially enhanced.


口試委員會審定書 #
誌謝 i
中文摘要 ii
ABSTRACT iv
CONTENTS vi
LIST OF FIGURES ix
LIST OF TABLES xi
Chapter 1 Introduction 1
1.1 Problem Formulation and Supported Constraint Types 3
1.1.1 CRV Problem Formulation 3
1.1.2 Supported Constraint Types 3
1.1.3 Difference between Constraint Satisfaction and Constraint Verification Problem. 3
1.2 Related Work 4
1.3 Contribution 8
Chapter 2 Review of RSSDE technique 9
2.1 Flow of RSSDE 9
2.2 Preprocessing Stage (RST Construction) 11
2.2.1 Properties of Range Splitting Tree (RST) 11
2.2.2 Solution Density Estimation by Statistical Approach 12
2.2.3 RST Construction Heuristics 12
2.3 RST Guided Pattern Generation Stage 15
2.4 RSSDE Algorithm 16
Chapter 3 Global and Local Infeasible Space Identification 19
3.1 Applicability of Global and Local Infeasible Space Identification 21
3.2 Global Infeasible Space Identification 27
3.2.1 Brute-Force Approach 28
3.2.2 Depth-Limited Bisection Approach (Single SMT instance) 28
3.2.3 Iterative Event-Driven Approach (Multiple STM instances) 31
3.3 Local Infeasible Space Identification 36
3.3.1 Split by Constant Values 38
3.3.2 Split by Infeasible Intervals Detection 39
3.3.3 Split by Joint Distribution Analysis of Two Variables 42
3.3.4 Split by Random Bisection 45
Chapter 4 Discussions and Heuristics 46
4.1 Direct Branching Probabilities Estimation by Using Only Leaf Nodes 46
4.2 Adaptive Cutting Plane Decision by Biased Distribution 47
4.3 Parallel RSTs 48
4.3.1 Independent Variables Case 48
4.3.2 Dependent Variables Case 49
4.4 Direct Constraint-based Infeasible Space Inference 50
Chapter 5 Experimental Results 51
5.1 Description of Testcases 51
5.2 Evaluation of Efficiency and Effectiveness of Infeasible Space Identification 53
5.2.1 Comparison of our approach and RSSDE 53
5.2.2 Comparison of Depth-Limited and Iterative Event-Driven Approaches at Global Identification Stage 56
5.2.3 Comparison of Different SMT Construction Methods at Local Identification Stage 59
5.3 Evaluation of Throughput, Evenness and Pattern Diversity 62
Chapter 6 Conclusion 65
REFERENCES 66


[1]SystemVerilog LRM can be found at http://www.systemverilog.org.
[2]S. M. Plaza, I. L. Markov and V. Bertacco, "Random Stimulus Generation Using Entropy and XOR Constraints," conference on Design, Automation and Test in Europe (DATE), 2008.
[3]S. Deng, Z. Kong, J. Bian and Y. Zhao, "Self-Adjusting Constrained Random Stimulus Generation Using Splitting Evenness Evaluation and XOR Constraints," Asia and South Pacific Design Automation Conference (ASPDAC), 2009.
[4]B.-H. Wu, C.-J. Yang, C.-C. Tso and C.-Y. (Ric) Huang, “Toward an Extremely-High-Throughput and Even-Distribution Pattern Generator for the Constrained Random Simulation Techniques,” International Conference on Computer-Aided Design (ICCAD), pp. 602-607, 2011.
[5]L. Devroye, "Random Variate Generation for Unimodal and Monotone densities," Computing, pp.43-68, 1984
[6]J. Yuan, A. Aziz, C. Pixley, and K. Albin, “Simplifying Boolean Constraint Solving for Random Simulation-Vector Generation,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, pp. 412-420, 2004.
[7]N. Kitchen and A. Kuehlmann, “A Markov chain Monte Carlo Sampler for Mixed Boolean/integer Constraints,” in Computer Aided Verification (CAV), pp.446-461, 2009.
[8]C. P. Gomes, A. Sabharwal and B. Selman, ”Near-Uniform Sampling of Combinatorial Spaces Using XOR Constraints,” 20th Annual Conference on Neural Information Processing Systems, pp. 481-488, 2006.
[9]R. Brummayer and A. Biere, “Boolector: an Efficient SMT Solver for Bit-Vectors and Arrays,” 15th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2009.
[10]M. A. Iyer, “RACE: A Word-level ATPG-based Constraints Solver System for Smart Random Simulation,” in IEEE International Test Conference (ITC), pp. 299-308, 2003.
[11]B.-H. Wu, C.-J. Yang and C.Y. (Ric) Huang, “A High-Throughput and Arbitrary-Distribution Pattern Generator for the Constrained Random Verification,” IEEE Trans. on CAD of Integrated Circuits and Systems 33 (TCAD), pp. 139-152, 2014.
[12]Bo-Han Wu, “A High-Throughput and General-Distribution Pattern Generator for Constrained Random Verification” (Doctoral Dissertation), National Taiwan University, 2014.
[13]B.-H. Wu and C.-Y. (Ric) Huang, “A Robust General Constrained Random Pattern Generator for Constraints with Variable Ordering,” International Conference on Computer-Aided Design (ICCAD), pp. 109-114, 2012.
[14]N. Sorensson and N. Een, "Minisat v1. 13-A Sat Solver with Conflict-Clause Minimization," in SAT Competition, 2005, p. 53.
[15]An efficient k-means clustering algorithm: Analysis and implementation, T. Kanungo, D. M. Mount, N. Netanyahu, C. Piatko, R. Silverman, and A. Y. Wu, IEEE Trans. Pattern Analysis and Machine Intelligence, 24 (2002), 881-892.


QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
無相關論文
 
無相關期刊
 
無相關點閱論文