Constraint-Based Verification

Constraint-Based Verification covers an emerging field in functional verification of electronic designs, referred to as the "constraint-based verification. The topics are developed in the context of a wide range of dynamic and static verification approaches including simulation, emulation, and formal methods. The goal is to show how constraints, or assertions, can be used towards automating the generation of testbenches, resulting in a seamless verification flow. Topics such as verification coverage, and connection with assertion based verification, are also covered.The book targets verification engineers as well as researchers. It covers both methodological and technical issues. Particular stress is given to the latest advances in functional verification.The research community has witnessed recent growth of interests in constraint-based functional verification. Various techniques have been developed. They are relatively new, but have reached a level of maturity so that they are appearing in commercial tools such as Vera and System Verilog. Contents......Page 6 Dedication......Page 5 1. INTRODUCTION......Page 12 1.1 Design Complexity......Page 13 1.2 The Design Productivity Gap......Page 15 1.3 The Verification Crisis......Page 16 1.4 Design Modeling and Verification......Page 18 1.5 Dynamic versus Static Verification......Page 20 1.6.1 Simulators......Page 22 1.6.3 Test Generation......Page 23 1.6.5 Coverage......Page 24 1.7 Emulation......Page 25 1.8.1 Equivalence Checking......Page 26 1.8.2 Model Checking and Bounded Model Checking......Page 27 1.8.5 Symbolic Simulation......Page 28 1.9 Constraints, Assertions, and Verification......Page 29 1.9.1 Constrained Random Simulation......Page 30 1.10 A Composite Verification Strategy......Page 31 1.11 Summary and Book Organization......Page 32 2. CONSTRAINED RANDOM SIMULATION......Page 35 2.1 Constraints for Test Generation......Page 36 2.2 Constraining Design Behaviors......Page 39 2.3 Constraint Solving......Page 40 2.5 Randomization......Page 42 2.7.1 The Language......Page 43 2.7.3 Prioritized Constraints......Page 45 3. HIGH LEVEL VERIFICATION LANGUAGES......Page 46 3.1 Testbench and System Languages......Page 47 3.2.1 Constraints......Page 49 3.2.4 Dynamic Constraints and Randomization......Page 50 3.3 SystemVerilog Random Constraints......Page 51 3.3.1 Overview......Page 52 3.3.3 Inline Constraints......Page 54 3.3.4 Random Sequence Generation......Page 55 3.3.5 Variable ordering......Page 56 3.3.7 Guarded Constraints......Page 58 3.3.9 Pre-processing and Post-processing......Page 59 3.3.10 Random Stability......Page 60 3.4 Summary......Page 61 4. ASSERTION LANGUAGES AND CONSTRAINTS......Page 62 4.1.1 PSL......Page 63 4.1.2 OVL......Page 64 4.2 Temporal Logic and Regular Expression......Page 65 4.2.1 Temporal Logic......Page 66 4.2.2 Regular Expression......Page 67 4.2.3 Truthness of Properties......Page 68 4.2.4 Strong and Weak Semantics......Page 70 4.2.5 Safety and Liveness Properties......Page 72 4.3.1 The Four Layers of PSL......Page 74 4.3.2 Verification Units......Page 75 4.3.3 Sequential Extended Regular Expression......Page 76 4.3.4 The Foundation Language......Page 77 4.4.1 Monitors......Page 79 4.4.2 Generators......Page 82 4.5 Monitor Construction......Page 83 4.5.1 The Tableau Rules and Cover......Page 84 4.5.2 Constructing the NFA......Page 85 4.5.3 Determinization of NFA......Page 88 4.6 Summary......Page 89 5.1 Boolean Algebra and Notations......Page 91 5.2 Graphs......Page 92 5.3 Hardware Modeling......Page 93 5.4 Reachability Analysis......Page 96 5.5.1 BDD Representation of Boolean Functions......Page 98 5.5.2 BDD Manipulations......Page 99 5.5.3 The BDD Size Consideration......Page 100 5.6 Boolean Satisfiability......Page 101 5.6.1 SAT Solving......Page 102 5.6.2 Definitions......Page 103 5.6.3 Conflict-based learning and Backtracking......Page 105 5.6.4 Decision Heuristics......Page 108 5.6.5 Efficient BCP Implementation......Page 109 5.6.6 Unsatisfiable Core......Page 110 5.6.7 Other Optimizations......Page 111 5.7 Automatic Test Pattern Generation......Page 112 5.7.1 The D-algorithm......Page 113 5.7.2 The PODEM and FAN algorithms......Page 114 6. CONSTRAINED VECTOR GENERATION......Page 116 6.1.1 BDD Representation of Constraints......Page 117 6.1.3 Constrained Probabilities......Page 118 6.1.4 An Example of Constrained Probability......Page 119 6.2 Simulation Vector Generation......Page 120 6.2.1 The Weight Procedure......Page 121 6.2.2 The Walk Procedure......Page 122 6.2.3 Correctness and Properties......Page 124 6.3.2 Constraint Partitioning......Page 127 6.4 Variable Solve Order......Page 128 6.5 Weighted Distribution......Page 131 6.6 Cycling Variables and Permutations......Page 132 6.8 Results......Page 133 6.8.1 Constraint BDDs......Page 134 6.8.2 A Case Study......Page 135 6.9 Summary......Page 137 7. CONSTRAINT SIMPLIFICATION......Page 139 7.1 Definitions......Page 141 7.2 Syntactical Extraction......Page 143 7.3 Functional Extraction......Page 145 7.4 Constraint Simplification......Page 148 7.4.1 Recursive Extraction......Page 149 7.6 Historical Perspective......Page 151 7.7.1 Impact on Building Conjunction BDDs......Page 154 7.7.2 Impact on Simulation......Page 156 7.8 Summary......Page 157 8. MORE OPTIMIZATIONS......Page 159 8.0.1 Constraint Prioritization......Page 160 8.0.2 Tree-decomposition......Page 161 8.0.3 Functional Decomposition......Page 163 8.0.4 Formula Factorization......Page 164 8.1 Implication of Multiple Clocks......Page 165 8.2 Summary......Page 166 9. CONSTRAINT SYNTHESIS......Page 167 9.1 Problem Formulation......Page 168 9.2 The Constraint Synthesis Method......Page 170 9.2.1 Deriving Reproductive Solutions......Page 171 9.2.2 Don't Cares......Page 173 9.2.3 Variable Removal......Page 174 9.2.4 The Overall Algorithm......Page 175 9.3 Other Synthesis Methods......Page 176 9.4 Coudert and Madre's Method......Page 177 9.4.1 Randomization......Page 180 9.5.1 Computing the Weights......Page 181 9.5.2 Computing the Assignments......Page 182 9.6 Synthesis using SAT solving......Page 183 9.7 Experimental Results......Page 185 9.8 Summary and Discussion......Page 187 10. CONSTRAINT DIAGNOSIS......Page 189 10.1 The Illegal States......Page 190 10.3 Locating the Conflict Source......Page 191 10.4 Fixing Over-constraints via Illegal States Removal......Page 192 10.5 Summary......Page 193 11. WORD-LEVEL CONSTRAINT SOLVING......Page 194 11.1 DPLL-based 01-ILP......Page 197 11.1.1 Linear Pseudo Boolean Constraints......Page 198 11.1.2 Cutting-planes in ILP......Page 199 11.1.3 A DPLL-based 01-ILP Algorithm......Page 201 11.2 Multi-valued Satisfiability......Page 208 11.3 Word-level Constraint Solving......Page 210 11.3.1 Converting RTL to Integer Linear Constraints......Page 211 11.3.2 Propagation and Implication......Page 216 11.3.3 Lazy Evaluation......Page 218 11.3.5 Conflict Analysis......Page 219 11.3.6 Arithmetic Solving......Page 221 11.4 ATPG-based Word-level Constraint Solving......Page 222 11.6 Summary......Page 225 A. Acronyms......Page 226 B.1 Proofs for Chapter 6......Page 228 B.2 Proofs for Chapter 7......Page 231 B.3 Proofs for Chapter 8......Page 234 References......Page 236 B......Page 252 C......Page 253 F......Page 254 M......Page 255 R......Page 256 T......Page 257 Z......Page 258 Contents 6 Dedication 5 1. INTRODUCTION 12 1.1 Design Complexity 13 1.2 The Design Productivity Gap 15 1.3 The Verification Crisis 16 1.4 Design Modeling and Verification 18 1.5 Dynamic versus Static Verification 20 1.6 Simulation 22 1.6.1 Simulators 22 1.6.2 Testbench 23 1.6.3 Test Generation 23 1.6.4 Checking Strategies 24 1.6.5 Coverage 24 1.7 Emulation 25 1.8 Static Verification 26 1.8.1 Equivalence Checking 26 1.8.2 Model Checking and Bounded Model Checking 27 1.8.3 Theorem Proving 28 1.8.4 Language Containment 28 1.8.5 Symbolic Simulation 28 1.8.6 Hybrid Simulation and Formal Verification 29 1.9 Constraints, Assertions, and Verification 29 1.9.1 Constrained Random Simulation 30 1.9.2 Assertion-based Verification 31 1.10 A Composite Verification Strategy 31 1.11 Summary and Book Organization 32 2. CONSTRAINED RANDOM SIMULATION 35 2.1 Constraints for Test Generation 36 2.2 Constraining Design Behaviors 39 2.3 Constraint Solving 40 2.4 Efficiency of Constraint Solving 42 2.5 Randomization 42 2.6 Constraint Diagnosis 43 2.7 A Constrained Random Simulation Tool 43 2.7.1 The Language 43 2.7.2 BDD-based Constraint Solving 45 2.7.3 Prioritized Constraints 45 3. HIGH LEVEL VERIFICATION LANGUAGES 46 3.1 Testbench and System Languages 47 3.2 Constrained Random Simulation Languages 49 3.2.1 Constraints 49 3.2.2 Commutativity of Constraints 50 3.2.3 Randomization 50 3.2.4 Dynamic Constraints and Randomization 50 3.3 SystemVerilog Random Constraints 51 3.3.1 Overview 52 3.3.2 Set Membership 54 3.3.3 Inline Constraints 54 3.3.4 Random Sequence Generation 55 3.3.5 Variable ordering 56 3.3.6 Cycling Random Variables and Permutations 58 3.3.7 Guarded Constraints 58 3.3.8 Distribution 59 3.3.9 Pre-processing and Post-processing 59 3.3.10 Random Stability 60 3.3.11 Dynamic Constraints and Randomization 61 3.4 Summary 61 4. ASSERTION LANGUAGES AND CONSTRAINTS 62 4.1 Assertion Languages 63 4.1.1 PSL 63 4.1.2 OVL 64 4.2 Temporal Logic and Regular Expression 65 4.2.1 Temporal Logic 66 4.2.2 Regular Expression 67 4.2.3 Truthness of Properties 68 4.2.4 Strong and Weak Semantics 70 4.2.5 Safety and Liveness Properties 72 4.2.6 Multiple Paths and Initial States 74 4.3 Introduction to PSL 74 4.3.1 The Four Layers of PSL 74 4.3.2 Verification Units 75 4.3.3 Sequential Extended Regular Expression 76 4.3.4 The Foundation Language 77 4.4 Monitors and Generators 79 4.4.1 Monitors 79 4.4.2 Generators 82 4.5 Monitor Construction 83 4.5.1 The Tableau Rules and Cover 84 4.5.2 Constructing the NFA 85 4.5.3 Determinization of NFA 88 4.6 Summary 89 5. PRELIMINARIES 91 5.1 Boolean Algebra and Notations 91 5.2 Graphs 92 5.3 Hardware Modeling 93 5.4 Reachability Analysis 96 5.5 Reduced Ordered Binary Decision Diagrams 98 5.5.1 BDD Representation of Boolean Functions 98 5.5.2 BDD Manipulations 99 5.5.3 The BDD Size Consideration 100 5.6 Boolean Satisfiability 101 5.6.1 SAT Solving 102 5.6.2 Definitions 103 5.6.3 Conflict-based learning and Backtracking 105 5.6.4 Decision Heuristics 108 5.6.5 Efficient BCP Implementation 109 5.6.6 Unsatisfiable Core 110 5.6.7 Other Optimizations 111 5.7 Automatic Test Pattern Generation 112 5.7.1 The D-algorithm 113 5.7.2 The PODEM and FAN algorithms 114 6. CONSTRAINED VECTOR GENERATION 116 6.1 Constraints and Biasing 117 6.1.1 BDD Representation of Constraints 117 6.1.2 Input Biasing and Vector Distribution 118 6.1.3 Constrained Probabilities 118 6.1.4 An Example of Constrained Probability 119 6.2 Simulation Vector Generation 120 6.2.1 The Weight Procedure 121 6.2.2 The Walk Procedure 122 6.2.3 Correctness and Properties 124 6.3 Implementation Issues 127 6.3.1 Variable Ordering 127 6.3.2 Constraint Partitioning 127 6.3.3 The Overall Flow 128 6.4 Variable Solve Order 128 6.5 Weighted Distribution 131 6.6 Cycling Variables and Permutations 132 6.7 Historical Perspective 133 6.8 Results 133 6.8.1 Constraint BDDs 134 6.8.2 A Case Study 135 6.9 Summary 137 7. CONSTRAINT SIMPLIFICATION 139 7.1 Definitions 141 7.2 Syntactical Extraction 143 7.3 Functional Extraction 145 7.4 Constraint Simplification 148 7.4.1 Recursive Extraction 149 7.5 The Overall Algorithm 151 7.6 Historical Perspective 151 7.7 Experiments 154 7.7.1 Impact on Building Conjunction BDDs 154 7.7.2 Impact on Simulation 156 7.8 Summary 157 8. MORE OPTIMIZATIONS 159 8.0.1 Constraint Prioritization 160 8.0.2 Tree-decomposition 161 8.0.3 Functional Decomposition 163 8.0.4 Formula Factorization 164 8.1 Implication of Multiple Clocks 165 8.2 Summary 166 9. CONSTRAINT SYNTHESIS 167 9.1 Problem Formulation 168 9.2 The Constraint Synthesis Method 170 9.2.1 Deriving Reproductive Solutions 171 9.2.2 Don't Cares 173 9.2.3 Variable Removal 174 9.2.4 The Overall Algorithm 175 9.3 Other Synthesis Methods 176 9.4 Coudert and Madre's Method 177 9.4.1 Randomization 180 9.5 Building Circuits from Relations 181 9.5.1 Computing the Weights 181 9.5.2 Computing the Assignments 182 9.5.3 Selecting the Outputs 183 9.6 Synthesis using SAT solving 183 9.7 Experimental Results 185 9.8 Summary and Discussion 187 10. CONSTRAINT DIAGNOSIS 189 10.1 The Illegal States 190 10.2 Reachability Analysis 191 10.3 Locating the Conflict Source 191 10.4 Fixing Over-constraints via Illegal States Removal 192 10.5 Summary 193 11. WORD-LEVEL CONSTRAINT SOLVING 194 11.1 DPLL-based 01-ILP 197 11.1.1 Linear Pseudo Boolean Constraints 198 11.1.2 Cutting-planes in ILP 199 11.1.3 A DPLL-based 01-ILP Algorithm 201 11.2 Multi-valued Satisfiability 208 11.3 Word-level Constraint Solving 210 11.3.1 Converting RTL to Integer Linear Constraints 211 11.3.2 Propagation and Implication 216 11.3.3 Lazy Evaluation 218 11.3.4 Multiple Domain Reductions 219 11.3.5 Conflict Analysis 219 11.3.6 Arithmetic Solving 221 11.4 ATPG-based Word-level Constraint Solving 222 11.5 Randomization Consideration 225 11.6 Summary 225 Appendices 226 A. Acronyms 226 B. Proofs 228 B.1 Proofs for Chapter 6 228 B.2 Proofs for Chapter 7 231 B.3 Proofs for Chapter 8 234 References 236 Index 252 A 252 B 252 C 253 D 254 E 254 F 254 G 255 H 255 I 255 J 255 K 255 L 255 M 255 N 256 O 256 P 256 R 256 S 257 T 257 U 258 V 258 W 258 Z 258 Constraint-Based Verification covers an emerging field in functional verification of electronic designs, referred to as the'constraint-based verification.'The topics are developed in the context of a wide range of dynamic and static verification approaches including simulation, emulation, and formal methods. The goal is to show how constraints, or assertions, can be used towards automating the generation of testbenches, resulting in a seamless verification flow. Topics such as verification coverage, and connection with assertion based verification, are also covered. The book targets verification engineers as well as researchers. It covers both methodological and technical issues. Particular stress is given to the latest advances in functional verification. The research community has witnessed recent growth of interests in constraint-based functional verification. Various techniques have been developed. They are relatively new, but have reached a level of maturity so that they are appearing in commercial tools such as Vera and System Verilog. Constraint-Based Verification covers the emerging field in functional verification of electronic designs that is now commonly referred to by this name.Topics are developed in the context of a wide range of dynamic and static verification approaches including stimulation, emulation and formal methods. The goal is to show how constraints, or assertions, can be used toward automating the generation of testbenches resulting in a seamless verification flow. Topics such as verification coverage and connection with assertion-based verification are also covered.Constraint-Based Verification is written for verification engineers, as well as researchers. This book discusses both methodological and technical issues. Particular stress is given to the latest advances in functional verification. Covers a field in functional verification of electronic designs, referred to as the "constraint-based verification." This book aims to show how constraints, or assertions, can be used towards automating the generation of testbenches, resulting in a seamless verification flow. It is aimed at verification engineers as well as researchers Covers the methodology and state-of-the-art techniques of constrained verification, which is new and popular. It relates constrained verification with the also-hot technology called assertion-based design. Discussed and clarifies language issues, critical to both the above, which will help the implementation of these languages. "Constraint-Based Verification is written for verification engineers, as well as researchers. This book discusses both methodological and technical issues. Particular stress is given to the latest advances in functional verification."--Résumé de l'éditeur