| Dedication | p. v |
| Introduction | p. 1 |
| Design Complexity | p. 2 |
| The Design Productivity Gap | p. 4 |
| The Verification Crisis | p. 5 |
| Design Modeling and Verification | p. 7 |
| Dynamic versus Static Verification | p. 9 |
| Simulation | p. 11 |
| Simulators | p. 11 |
| Testbench | p. 12 |
| Test Generation | p. 12 |
| Checking Strategies | p. 13 |
| Coverage | p. 13 |
| Emulation | p. 14 |
| Static Verification | p. 15 |
| Equivalence Checking | p. 15 |
| Model Checking and Bounded Model Checking | p. 16 |
| Theorem Proving | p. 17 |
| Language Containment | p. 17 |
| Symbolic Simulation | p. 17 |
| Hybrid Simulation and Formal Verification | p. 18 |
| Constraints, Assertions, and Verification | p. 18 |
| Constrained Random Simulation | p. 19 |
| Assertion-based Verification | p. 20 |
| A Composite Verification Strategy | p. 20 |
| Summary and Book Organization | p. 21 |
| Constrained Random Simulation | p. 25 |
| Constraints for Test Generation | p. 26 |
| Constraining Design Behaviors | p. 29 |
| Constraint Solving | p. 30 |
| Efficiency of Constraint Solving | p. 32 |
| Randomization | p. 32 |
| Constraint Diagnosis | p. 33 |
| A Constrained Random Simulation Tool | p. 33 |
| The Language | p. 33 |
| BDD-based Constraint Solving | p. 35 |
| Prioritized Constraints | p. 35 |
| High Level Verification Languages | p. 37 |
| Testbench and System Languages | p. 38 |
| Constrained Random Simulation Languages | p. 40 |
| Constraints | p. 40 |
| Commutativity of Constraints | p. 41 |
| Randomization | p. 41 |
| Dynamic Constraints and Randomization | p. 41 |
| System Verilog Random Constraints | p. 42 |
| Overview | p. 43 |
| Set Membership | p. 45 |
| Inline Constraints | p. 45 |
| Random Sequence Generation | p. 46 |
| Variable ordering | p. 47 |
| Cycling Random Variables and Permutations | p. 49 |
| Guarded Constraints | p. 49 |
| Distribution | p. 50 |
| Pre-processing and Post-processing | p. 50 |
| Random Stability | p. 51 |
| Dynamic Constraints and Randomization | p. 52 |
| Summary | p. 52 |
| Assertion Languages and Constraints | p. 53 |
| Assertion Languages | p. 54 |
| PSL | p. 54 |
| OVL | p. 55 |
| Temporal Logic and Regular Expression | p. 56 |
| Temporal Logic | p. 57 |
| Regular Expression | p. 58 |
| Truthness of Properties | p. 59 |
| Strong and Weak Semantics | p. 61 |
| Safety and Liveness Properties | p. 63 |
| Multiple Paths and Initial States | p. 65 |
| Introduction to PSL | p. 65 |
| The Four Layers of PSL | p. 65 |
| Verification Units | p. 66 |
| Sequential Extended Regular Expression | p. 67 |
| Teh Foundation Language | p. 68 |
| Monitors and Generators | p. 70 |
| Monitors | p. 70 |
| Generators | p. 73 |
| Monitor Construction | p. 74 |
| The Tableau Rules and Cover | p. 75 |
| Constructing the NFA | p. 76 |
| Determinization of NFA | p. 79 |
| Summary | p. 80 |
| Preliminaries | p. 83 |
| Boolean Algebra and Notations | p. 83 |
| Graphs | p. 84 |
| Hardware Modeling | p. 85 |
| Reachability Analysis | p. 88 |
| Reduced Ordered Binary Decision Diagrams | p. 90 |
| BDD Representation of Boolean Functions | p. 90 |
| BDD Manipulations | p. 91 |
| The BDD Size Consideration | p. 92 |
| Boolean Satisfiability | p. 93 |
| SAT Solving | p. 94 |
| Definitions | p. 95 |
| Conflict-based learning and Backtracking | p. 97 |
| Decision Heuristics | p. 100 |
| Efficient BCP Implementation | p. 101 |
| Unsatisfiable Core | p. 102 |
| Other Optimizations | p. 103 |
| Automatic Test Pattern Generation | p. 104 |
| The D-algorithm | p. 105 |
| The PODEM and FAN algorithms | p. 106 |
| Constrained Vector Generation | p. 109 |
| Constraints and Biasing | p. 110 |
| BDD Representation of Constraints | p. 110 |
| Input Biasing and Vector Distribution | p. 111 |
| Constrained Probabilities | p. 111 |
| An Example of Constrained Probability | p. 112 |
| Simulation Vector Generation | p. 113 |
| The Weight Procedure | p. 114 |
| The Walk Procedure | p. 115 |
| Correctness and Properties | p. 117 |
| Implementation Issues | p. 120 |
| Variable Ordering | p. 120 |
| Constraint Partitioning | p. 120 |
| The Overall Flow | p. 121 |
| Variable Solve Order | p. 121 |
| Weighted Distribution | p. 124 |
| Cycling Variables and Permutations | p. 125 |
| Historical Perspective | p. 126 |
| Results | p. 126 |
| Constraint BDDs | p. 127 |
| A Case Study | p. 128 |
| Summary | p. 130 |
| Constraint Simplification | p. 133 |
| Definitions | p. 135 |
| Syntactical Extraction | p. 137 |
| Functional Extraction | p. 139 |
| Constraint Simplification | p. 142 |
| Recursive Extraction | p. 143 |
| The Overall Algorithm | p. 145 |
| Historical Perspective | p. 145 |
| Experiments | p. 148 |
| Impact on Building Conjunction BDDs | p. 148 |
| Impact on Simulation | p. 150 |
| Summary | p. 151 |
| More Optimizations | p. 153 |
| Constraint Prioritization | p. 154 |
| Tree-decomposition | p. 155 |
| Functional Decomposition | p. 157 |
| Formula Factorization | p. 158 |
| Implication of Multiple Clocks | p. 159 |
| Summary | p. 160 |
| Constraint Synthesis | p. 161 |
| Problem Formulation | p. 162 |
| The Constraint Synthesis Method | p. 164 |
| Deriving Reproductive Solutions | p. 165 |
| Don't Cares | p. 167 |
| Variable Removal | p. 168 |
| The Overall Algorithm | p. 169 |
| Other Synthesis Methods | p. 170 |
| Coudert and Madre's Method | p. 171 |
| Randomization | p. 174 |
| Building Circuits from Relations | p. 175 |
| Computing the Weights | p. 175 |
| Computing the Assignments | p. 176 |
| Selecting the Outputs | p. 177 |
| Synthesis using SAT solving | p. 177 |
| Experimental Results | p. 179 |
| Summary and Discussion | p. 181 |
| Constraint Diagnosis | p. 183 |
| The Illegal States | p. 184 |
| Reachability Analysis | p. 185 |
| Locating the Conflict Source | p. 185 |
| Fixing Over-constraints via Illegal States Removal | p. 186 |
| Summary | p. 187 |
| Word-Level Constraint Solving | p. 189 |
| DPLL-based 01-ILP | p. 192 |
| Linear Pseudo Boolean Constraints | p. 193 |
| Cutting-planes in ILP | p. 194 |
| A DPLL-based 01-ILP Algorithm | p. 196 |
| Multi-valued Satisfiability | p. 203 |
| Word-level Constraint Solving | p. 205 |
| Converting RTL to Integer Linear Constraints | p. 206 |
| Propagation and Implication | p. 211 |
| Lazy Evaluation | p. 213 |
| Multiple Domain Reductions | p. 214 |
| Conflict Analysis | p. 214 |
| Arithmetic Solving | p. 216 |
| ATPG-based Word-level Constraint Solving | p. 217 |
| Randomization Consideration | p. 220 |
| Summary | p. 220 |
| Appendices | p. 221 |
| Acronyms | p. 221 |
| Proofs | p. 223 |
| Proofs for Chapter 6 | p. 223 |
| Proofs for Chapter 7 | p. 226 |
| Proofs for Chapter 8 | p. 229 |
| References | p. 231 |
| Index | p. 247 |
| Table of Contents provided by Ingram. All Rights Reserved. |
