Constraint-based Verification

by Yuan, Jun; Pixley, Carl; Aziz, Adnan

• ISBN13: 9780387259475
• ISBN10: 0387259473
• Format: Hardcover
• Copyright: 2005-10-01
• Publisher: Springer Verlag

Summary

Constraint-Based Verification covers the emerging field in functional verification of electronic designs that is now commonly referred to by this name.

Table of Contents

Dedication	v
1. INTRODUCTION	1	(24)
1.1 Design Complexity	2	(2)
1.2 The Design Productivity Gap	4	(1)
1.3 The Verification Crisis	5	(2)
1.4 Design Modeling and Verification	7	(2)
1.5 Dynamic versus Static Verification	9	(2)
1.6 Simulation	11	(3)
1.6.1 Simulators	11	(1)
1.6.2 Testbench	12	(1)
1.6.3 Test Generation	12	(1)
1.6.4 Checking Strategies	13	(1)
1.6.5 Coverage	13	(1)
1.7 Emulation	14	(1)
1.8 Static Verification	15	(3)
1.8.1 Equivalence Checking	15	(1)
1.8.2 Model Checking and Bounded Model Checking	16	(1)
1.8.3 Theorem Proving	17	(1)
1.8.4 Language Containment	17	(1)
1.8.5 Symbolic Simulation	17	(1)
1.8.6 Hybrid Simulation and Formal Verification	18	(1)
1.9 Constraints, Assertions, and Verification	18	(2)
1.9.1 Constrained Random Simulation	19	(1)
1.9.2 Assertion-based Verification	20	(1)
1.10 A Composite Verification Strategy	20	(1)
1.11 Summary and Book Organization	21	(4)
2. CONSTRAINED RANDOM SIMULATION	25	(12)
2.1 Constraints for Test Generation	26	(3)
2.2 Constraining Design Behaviors	29	(1)
2.3 Constraint Solving	30	(2)
2.4 Efficiency of Constraint Solving	32	(1)
2.5 Randomization	32	(1)
2.6 Constraint Diagnosis	33	(1)
2.7 A Constrained Random Simulation Tool	33	(4)
2.7.1 The Language	33	(2)
2.7.2 BDD-based Constraint Solving	35	(1)
2.7.3 Prioritized Constraints	35	(2)
3. HIGH LEVEL VERIFICATION LANGUAGES	37	(16)
3.1 Testbench and System Languages	38	(2)
3.2 Constrained Random Simulation Languages	40	(2)
3.2.1 Constraints	40	(1)
3.2.2 Commutativity of Constraints	41	(1)
3.2.3 Randomization	41	(1)
3.2.4 Dynamic Constraints and Randomization	41	(1)
3.3 SystemVerilog Random Constraints	42	(10)
3.3.1 Overview	43	(2)
3.3.2 Set Membership	45	(1)
3.3.3 Inline Constraints	45	(1)
3.3.4 Random Sequence Generation	46	(1)
3.3.5 Variable ordering	47	(2)
3.3.6 Cycling Random Variables and Permutations	49	(1)
3.3.7 Guarded Constraints	49	(1)
3.3.8 Distribution	50	(1)
3.3.9 Pre-processing and Post-processing	50	(1)
3.3.10 Random Stability	51	(1)
3.3.11 Dynamic Constraints and Randomization	52	(1)
3.4 Summary	52	(1)
4. ASSERTION LANGUAGES AND CONSTRAINTS	53	(30)
4.1 Assertion Languages	54	(2)
4.1.1 PSL	54	(1)
4.1.2 OVL	55	(1)
4.2 Temporal Logic and Regular Expression	56	(9)
4.2.1 Temporal Logic	57	(1)
4.2.2 Regular Expression	58	(1)
4.2.3 Truthness of Properties	59	(2)
4.2.4 Strong and Weak Semantics	61	(2)
4.2.5 Safety and Liveness Properties	63	(2)
4.2.6 Multiple Paths and Initial States	65	(1)
4.3 Introduction to PSL	65	(5)
4.3.1 The Four Layers of PSL	65	(1)
4.3.2 Verification Units	66	(1)
4.3.3 Sequential Extended Regular Expression	67	(1)
4.3.4 The Foundation Language	68	(2)
4.4 Monitors and Generators	70	(4)
4.4.1 Monitors	70	(3)
4.4.2 Generators	73	(1)
4.5 Monitor Construction	74	(6)
4.5.1 The Tableau Rules and Cover	75	(1)
4.5.2 Constructing the NFA	76	(3)
4.5.3 Determinization of NFA	79	(1)
4.6 Summary	80	(3)
5. PRELIMINARIES	83	(26)
5.1 Boolean Algebra and Notations	83	(1)
5.2 Graphs	84	(1)
5.3 Hardware Modeling	85	(3)
5.4 Reachability Analysis	88	(2)
5.5 Reduced Ordered Binary Decision Diagrams	90	(3)
5.5.1 BDD Representation of Boolean Functions	90	(1)
5.5.2 BDD Manipulations	91	(1)
5.5.3 The BDD Size Consideration	92	(1)
5.6 Boolean Satisfiability	93	(11)
5.6.1 SAT Solving	94	(1)
5.6.2 Definitions	95	(2)
5.6.3 Conflict-based learning and Backtracking	97	(3)
5.6.4 Decision Heuristics	100	(1)
5.6.5 Efficient BCP Implementation	101	(1)
5.6.6 Unsatisfiable Core	102	(1)
5.6.7 Other Optimizations	103	(1)
5.7 Automatic Test Pattern Generation	104	(5)
5.7.1 The D-algorithm	105	(1)
5.7.2 The PODEM and FAN algorithms	106	(3)
6. CONSTRAINED VECTOR GENERATION	109	(24)
6.1 Constraints and Biasing	110	(3)
6.1.1 BDD Representation of Constraints	110	(1)
6.1.2 Input Biasing and Vector Distribution	111	(1)
6.1.3 Constrained Probabilities	111	(1)
6.1.4 An Example of Constrained Probability	112	(1)
6.2 Simulation Vector Generation	113	(7)
6.2.1 The Weight Procedure	114	(1)
6.2.2 The Walk Procedure	115	(2)
6.2.3 Correctness and Properties	117	(3)
6.3 Implementation Issues	120	(1)
6.3.1 Variable Ordering	120	(1)
6.3.2 Constraint Partitioning	120	(1)
6.3.3 The Overall Flow	121	(1)
6.4 Variable Solve Order	121	(3)
6.5 Weighted Distribution	124	(1)
6.6 Cycling Variables and Permutations	125	(1)
6.7 Historical Perspective	126	(1)
6.8 Results	126	(4)
6.8.1 Constraint BDDs	127	(1)
6.8.2 A Case Study	128	(2)
6.9 Summary	130	(3)
7. CONSTRAINT SIMPLIFICATION	133	(20)
7.1 Definitions	135	(2)
7.2 Syntactical Extraction	137	(2)
7.3 Functional Extraction	139	(3)
7.4 Constraint Simplification	142	(3)
7.4.1 Recursive Extraction	143	(2)
7.5 The Overall Algorithm	145	(1)
7.6 Historical Perspective	145	(3)
7.7 Experiments	148	(3)
7.7.1 Impact on Building Conjunction BDDs	148	(2)
7.7.2 Impact on Simulation	150	(1)
7.8 Summary	151	(2)
8. MORE OPTIMIZATIONS	153	(8)
8.0.1 Constraint Prioritization	154	(1)
8.0.2 Tree-decomposition	155	(2)
8.0.3 Functional Decomposition	157	(1)
8.0.4 Formula Factorization	158	(1)
8.1 Implication of Multiple Clocks	159	(1)
8.2 Summary	160	(1)
9. CONSTRAINT SYNTHESIS	161	(22)
9.1 Problem Formulation	162	(2)
9.2 The Constraint Synthesis Method	164	(6)
9.2.1 Deriving Reproductive Solutions	165	(2)
9.2.2 Don't Cares	167	(1)
9.2.3 Variable Removal	168	(1)
9.2.4 The Overall Algorithm	169	(1)
9.3 Other Synthesis Methods	170	(1)
9.4 Coudert and Madre's Method	171	(4)
9.4.1 Randomization	174	(1)
9.5 Building Circuits from Relations	175	(2)
9.5.1 Computing the Weights	175	(1)
9.5.2 Computing the Assignments	176	(1)
9.5.3 Selecting the Outputs	177	(1)
9.6 Synthesis using SAT solving	177	(2)
9.7 Experimental Results	179	(2)
9.8 Summary and Discussion	181	(2)
10. CONSTRAINT DIAGNOSIS	183	(6)
10.1 The Illegal States	184	(1)
10.2 Reachability Analysis	185	(1)
10.3 Locating the Conflict Source	185	(1)
10.4 Fixing Over-constraints via Illegal States Removal	186	(1)
10.5 Summary	187	(2)
11. WORD-LEVEL CONSTRAINT SOLVING	189	(32)
11.1 DPLL-based 01-ILP	192	(11)
11.1.1 Linear Pseudo Boolean Constraints	193	(1)
11.1.2 Cutting-planes in ILP	194	(2)
11.1.3 A DPLL-based 01-ILP Algorithm	196	(7)
11.2 Multi-valued Satisfiability	203	(2)
11.3 Word-level Constraint Solving	205	(12)
11.3.1 Converting RTL to Integer Linear Constraints	206	(5)
11.3.2 Propagation and Implication	211	(2)
11.3.3 Lazy Evaluation	213	(1)
11.3.4 Multiple Domain Reductions	214	(1)
11.3.5 Conflict Analysis	214	(2)
11.3.6 Arithmetic Solving	216	(1)
11.4 ATPG-based Word-level Constraint Solving	217	(3)
11.5 Randomization Consideration	220	(1)
11.6 Summary	220	(1)
Appendices	221	(10)
A Acronyms	221	(2)
B Proofs	223	(8)
B.1 Proofs for Chapter 6	223	(3)
B.2 Proofs for Chapter 7	226	(3)
B.3 Proofs for Chapter 8	229	(2)
References	231	(16)
Index	247