請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/56010
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang Huang) | |
dc.contributor.author | Bo-Han Wu | en |
dc.contributor.author | 吳柏翰 | zh_TW |
dc.date.accessioned | 2021-06-16T05:12:56Z | - |
dc.date.available | 2015-09-03 | |
dc.date.copyright | 2014-09-03 | |
dc.date.issued | 2014 | |
dc.date.submitted | 2014-08-18 | |
dc.identifier.citation | [1] J. Bergeron, “Writing Testbenches; Functional Verification of HDL Models,” Kluwer Academic Publishers, ISBN: 978-0-7923-7766-5, 2000.
[2] M.G. Bartley, D. Galpin and T. Blackmore, 'A Comparison of Three Verification Techniques: Directed testing, Pseudo-random Testing and Property Checking,' Design Automation Conference (DAC), pp.819-823, 2002. [3] J. Yuan, C. Pixley and A. Aziz, “Constraint-based Verification,” Springer, 2006. [4] M. Benjamin, D. Geist, A. Hartman, Y. Wolfsthal, G. Mas and R. Smeets, 'A Study in Coverage-Driven Test Generation,' Design Automation Conference (DAC), pp.970-975, 1999. [5] S. Tasiran and K. Keutzer, 'Coverage Metrics for Functional Validation of Hardware Designs,' Design and Test of Computers, pp.36-45, 2001. [6] J. Y. Jou and C. Liu, “Coverage Analysis Techniques for Hdl Design Validation,” Proc. Asia Pacific Chip Design Languages, pp 48-55, 1999. [7] S. Katz, O. Grumberg and D. Geist, “Have I written enough properties? - A Method of Comparison between Specification and Implementation,” pp. 280-297, Springer, 1999. [8] M. R. Woodward, “Mutation Testing - An Evolving Technique,” IEE Colloquium on Software Testing for Critical Systems, pp. 3/1-3/6, 1990. [9] T. C. Lee and P. A. Hsiung, “Mutation Coverage Estimation for Model Checking,” Automated Technology for Verification and Analysis, pp. 354-368, Springer, 2004. [10] E. Bin, R. Emek, G. Shurek, and A. Ziv, “Using a Constraint Satisfaction Formulation and Solution Techniques for Random Test Program Generation,” IBM Systems Journal, pp. 386-402, 2002. [11] Y. Katz, M. Rimon and A. Ziv, 'Generating Instruction Streams Using Abstract CSP,' Design, Automation and Test in Europe Conference and Exhibition (DATE), pp.15-20, 12-16, 2012. [12] SystemVerilog LRM can be found at http://www.systemverilog.org. [13] J. Bergeron, E. Cerny, A. Hunter and A. Nightingale, “Verfication Methodology Manual for SystemVerilog,” Springer-Verlag, 2005. [14] IEEE Standard for SystemVerilog – Unified Hardware Design, Specification and Verification Language, IEEE Computer Society, IEEE Std 1800, 2005. [15] IEEE Standard for the Functional Verification language ‘e’, IEEE Computer Society, IEEE, IEEE Std 1647, 2006. [16] D. Robinson, “Aspect-Oriented Programming with the e Verification Language: A Pragmatic Guide for Testbench Developers,” Elseview Inc., 2007. [17] J. Yuan, K. Shultz, C. Pixley, H. Miller, and A. Aziz, “Modeling Design Constraints and Biasing in Simulation Using BDDs,” Digest Tech. Papers IEEE/ACM Int’l Conf. Computer-Aided Design, pp. 584–589, 1999. [18] 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. [19] N. Sorensson and N. Een, 'Minisat v1. 13-A Sat Solver with Conflict-Clause Minimization,' in SAT Competition, 2005, p. 53. [20] The Satisfiability Modulo Theories Library Organization: http://www.smtlib.org/ [21] 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. [22] S. Jha, R. Limaye, and S. A. Seshia, “Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic,” 21st International Conference on Computer-Aided verification (CAV), pp. 668-674, 2009. [23] P. Nuzzo, A. Puggelli, S. A. Seshia, and A. L. Sangiovanni-Vincentelli, “CalCS: SMT Solving for Non-linear Convex Constraints,” IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 71-79, 2010. [24] Y. Zhao, J. Bian, S. Deng and Z. Kong, 'Random Stimulus Generation with Self-tuning,' 13th International Conference on Computer Supported Cooperative Work in Design, 2009. [25] 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. [26] 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. [27] M. H. Liffiton and K. A. Sakallah, “On Finding all Minimally Unsatisfiable Subformulas,” Int’l Conf. on Theory and Applications of Satisfiability Testing, 2005. [28] J. Bailey and P. J. Stuckey, “Discovery of Minimal Unsatisfiable Subsets of Constraints Using Hitting Set Dualization,” 7th international conference on Practical Aspects of Declarative Languages (PADL), pp. 174-186, 2005. [29] L. Devroye, 'Random Variate Generation for Unimodal and Monotone densities,' Computing, pp.43-68, 1984 [30] 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. [31] X. U. Lin and Y. C. Berthe, 'A Comparative Study of Arc-Consistency Algorithms,' 2001. [32] Jussien, Narendra, R. Debruyne and P. Boizumault. 'Maintaining Arc-Consistency within Dynamic Backtracking,' Principles and Practice of Constraint Programming Springer, pp. 249-261, 2000. [33] Sabin, Daniel, and C. E. Eugene, 'Understanding and Improving the MAC Algorithm,' Principles and Practice of Constraint Programming Springer, pp. 167-181, 1997. [34] W. Wei, J. Erenrich, and B. Selman, “Towards Efficient Sampling: Exploiting Random Walk Strategies,” in Proc. Nat’l Conf. Artificial Intelligence, pp. 670–676, Jul. 2004. [35] B. Selman, H. A. Kautz, and B. Cohen, “Local Search Strategies for Satisfiability Testing,” in Proc. 2nd DIMACS Challenge on Cliques, Coloring, and Satisfiability, 1993. [36] N. Kitchen and A. Kuehlmann, “Stimulus Generation for Constrained Random Simulation,” International Conference on Computer-Aided Design (ICCAD), pp. 258-265, 2007 [37] 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. [38] N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller and E. Teller, “Equatoins of State Calculations by Fast Computing Machines,” J. Cjem. Phys. 21, pp. 1087-1092, 1970. [39] 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. [40] B.-H. Wu and C.-Y. (Ric) Huang, “A Robust Constraint Solving Framework for Multiple Constraint Sets in Constrained Random Verification,” Design Automation Conference (DAC), pp 1-7, 2013. [41] 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. [42] 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. [43] M. Davis, G. Logemann and D. Loveland, 'A Machine Program for Theorem Proving,' Communications of the ACM 5, pp. 394-397, 1962. [44] J. P. Marques-Silva and K. A. Sakallah, “GRASP: A New Search Algorithm for Satisfiability,” International Conference on Computer-Aided Design (ICCAD), pp. 220-227, 1996. [45] J.P. Marques-Silva and K.A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Transactions on Computers, pp. 506-521, 1999. [46] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang and S. Malik, “Chaff: Engineering an Efficient SAT Solver” Design Automation Conference (DAC), 2001. [47] N. E’en and A. Biere, “Effective Preprocessing in SAT Through Variable and Clause Elimination,” International Conference on Theory and Applications of Satisfiability Testing (SAT), 2005. [48] L. Ryan, “Efficient Algorithms for Clause-Learning SAT Solvers,” M.Sc. Thesis, Simon Fraser Univ., 2003. [49] H. Kim, H. Jin, K. Ravi, P. Spacek, J. Pierce, B. Kurshan and F. Somenzi, 'Application of Formal Word-Level Analysis to Constrained Random Simulation,' 20th International Conference on Computer Aided Verification (CAV), 2008. [50] 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. [51] C. P. Gomes, W. Hoeve, A. Sabharwal and B. Selman, ”Counting CSP Solutions Using Generalized XOR Constraints,” 22nd Conference on Artificial Intelligence, pp.204-209, July 2007. [52] L. G. Valiant and V. V. Vazirani, “NP is as Easy as Detecting Unique Solutions,” 17th Annual ACM symposium on Theory of computing, pp. 458-463, 1985. [53] A. J. Compton, ”An Algorithm for the Even Distribution of Entities in One Dimension,” Computer Journal, pp. 530-537,1985. [54] R. Bruni and A. Sassano, “Restoring Satisfiability or Maintaining Unsatisfiability by Finding Small Unsatisfiable Subformulae,” Electronic Notes in Discrete Mathematics, 2001. [55] L. Zhang and S. Malik, “Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula,” 6th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2003. [56] I. Lynce and J. Marques-Silva, “On Computing Minimum Unsatisfiable Cores,” 7th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2004. [57] S. P. Lloyd, 'Least squares quantization in PCM,' IEEE Transactions on Information Theory, 1982. [58] D. Arthur and S. Vassilvitskii, 'K-Means++: The Advantages of Careful Seeding,' 8th annual ACM-SIAM symposium on Discrete algorithms. pp. 1027-1035, 2007. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/56010 | - |
dc.description.abstract | 現今為了驗證某些系統性的性質,限制隨機驗證方法(CRV)逐漸成為主流。主要原因是CRV擁有更高的效率和更好的擴展性。在此驗證方法中,驗證工程師只須撰寫限制式來表達待驗證的環境,而不需繁瑣地描述每個模擬測試的數值。當撰寫完這些限制式後,可透過限制式求解器來求解這些限制式,產生滿足限制的測試數值,進而模擬整個電路。為了保證主要的驗證可以花費於模擬電路和確認觀測的性質對錯上,產生符合限制式之測試數值的過程只能耗費相對少量的計算資源。另一方面,為了保證最好的驗證品質,VDL標準要求產生的模擬數值分布必須要均勻或者是符合驗證工程師所設定的機率分布。
在此研究中,我們提出一個限制求解技術來加速模擬數值的產生過程。而此法我們簡稱為RSSDE技術。我們主要著重在克服以下三個挑戰:1) 產生模擬數值以及滿足機率分步的權衡 2) 驗證限制式中包含變數順序的條件 3) 驗證環境中包含多種限制式的不同組合。以上這些挑戰皆在業界驗證環境中時常出現,像是出現於UVM或VVM的驗證環境中。而我們提出的技術保證加速產生過程,且同時滿足驗證工程師所要求的模擬數值機率分布。實驗結果亦顯示,在與業界所開發的系統比較,我們所提出的技術擁有較高速率的模擬數值產生優勢。 | zh_TW |
dc.description.abstract | 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. | en |
dc.description.provenance | Made available in DSpace on 2021-06-16T05:12:56Z (GMT). No. of bitstreams: 1 ntu-103-D99943038-1.pdf: 2079877 bytes, checksum: eb34273ccbc6c67fdbe968d1a091eeba (MD5) Previous issue date: 2014 | en |
dc.description.tableofcontents | 口試委員會審定書 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 112 | |
dc.language.iso | en | |
dc.title | 在限制隨機驗證中的高速廣義分佈測試模式產生器 | zh_TW |
dc.title | A High-Throughput and General-Distribution Pattern Generator for Constrained Random Verification | en |
dc.type | Thesis | |
dc.date.schoolyear | 102-2 | |
dc.description.degree | 博士 | |
dc.contributor.oralexamcommittee | 江介宏(Jie-Hong Jiang),顏嘉志(Chia-Chih Yen),李建模(Chien-Mo Li),王凡(Farn Wang),王柏堯(Bo-Yao Wang) | |
dc.subject.keyword | 功能性驗證,CRV,SystemVerilog,樣式分布,限制求解, | zh_TW |
dc.subject.keyword | functional verification,CRV,SystemVerilog,pattern distribution,constraint solving,solving-order constraints, | en |
dc.relation.page | 118 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2014-08-18 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-103-1.pdf 目前未授權公開取用 | 2.03 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。