Practical Design Verification

Half-title......Page 3
Title......Page 5
Copyright......Page 6
Contents......Page 7
Contributors......Page 12
1.1 Introduction......Page 15
1.2 Techniques for Boolean reasoning......Page 16
1.2.1 Binary decision diagrams (BDDs)......Page 17
1.2.2 Boolean satisfiability checker......Page 20
1.2.3 Automatic test-pattern generation (ATPG) techniques......Page 22
1.3.1.1 Kripke structures......Page 25
1.3.2 Basic algorithms of CTL model checking......Page 28
1.3.3 Symbolic model checking......Page 30
1.3.4 Practical model checking......Page 34
1.4 Equivalence-checking techniques......Page 36
1.4.2 Latch-mapping problem......Page 37
1.4.3 Practical combinational equivalence checking......Page 38
1.4.4 Sequential equivalence checking (SEC)......Page 42
1.5 Techniques for higher-level design descriptions......Page 49
1.6 References......Page 61
2.1 Taxonomy for TLMs......Page 65
2.1.1 Granularity-based classification of TLMs......Page 66
2.1.1.1 Specification model......Page 68
2.1.1.2 Component-assembly model......Page 69
2.1.1.3 Bus-arbitration model......Page 70
2.1.1.5 Cycle-accurate computation model......Page 72
2.1.2 Objective-based classification......Page 74
2.2 Estimation-oriented TLMs......Page 76
2.2.2 Similarity to TLM......Page 77
2.2.4 Measurements......Page 78
2.3 Synthesis-oriented TLMs......Page 79
2.3.1.1 Synchronization......Page 81
2.3.1.2 Arbitration......Page 83
2.3.1.3 Addressing and data transfer......Page 85
2.3.1.4 UBC user functions......Page 88
2.3.2 Transducer......Page 89
2.3.2.2 Request behaviors......Page 91
2.3.2.3 IO behaviors......Page 92
2.3.3 Routing......Page 93
2.3.4.1 Processes......Page 94
2.3.5 Synthesizable TLMs in practice: MP3 decoder design......Page 97
2.3.5.1 Development time......Page 99
2.3.5.2 Validation time......Page 102
2.4 Related work on TLMs......Page 103
2.6 References......Page 104
3.1.1 Identifying what to check......Page 106
3.1.2 Classifying design behavior......Page 107
3.1.3 Observability and controllability......Page 110
3.2 Testbench verification components......Page 111
3.3 Assertion-based verification......Page 113
3.3.1.1 Consecutive repetition......Page 114
3.3.1.4 Sequence implication......Page 115
3.4 Assertion-based bus monitor example......Page 116
3.4.1 Basic write operation......Page 118
3.4.2 Basic read operation......Page 119
3.4.3 Unpipelined parallel bus interface requirements......Page 120
3.4.4 Unpipelined parallel bus interface coverage......Page 122
3.4.5 Analysis communication in the testbench......Page 124
3.5 Summary......Page 125
3.6 References......Page 126
4.1 Introduction......Page 127
4.2 Debugging tools......Page 128
4.2.1 Logic analyzers and pattern generators......Page 129
4.2.2 Power measurement......Page 130
4.2.5 Profilers......Page 131
4.3 Debugging commands......Page 132
4.5 Performance-oriented debugging......Page 133
4.6 Summary......Page 134
4.7 References......Page 135
5.1 Introduction......Page 136
5.2 Coverage metrics......Page 142
5.3.1.1 Statement coverage (SC)......Page 145
5.3.1.3 Condition coverage (CC)......Page 147
5.3.1.5 Path coverage (PC)......Page 148
5.3.2.1 Toggle coverage (TC)......Page 150
5.3.3.2 FSM state coverage (FSM-SC)......Page 151
5.3.4 Functional coverage metrics......Page 154
5.3.5.1 Mutation coverage (MC)......Page 155
5.3.6.1 Observability-based code coverage metric (OCCOM)......Page 157
5.4 Coverage metrics and abstraction levels of design......Page 158
5.5 Stimuli generation methods......Page 159
5.5.1 Manual generation......Page 160
5.5.2 Automatic generation......Page 161
5.5.2.1 Deterministic generation techniques......Page 162
5.5.2.2 Random generation techniques......Page 163
5.7 References......Page 165
6.1 Introduction......Page 168
6.2 Testbench components......Page 169
6.2.2.1 Input monitor......Page 170
6.2.3.2 Functional correctness checker......Page 171
6.2.4 Scoreboard......Page 172
6.2.5.2 Driver......Page 173
6.4.1 DUV......Page 174
6.4.3 Testbench......Page 177
6.5 Summary......Page 185
6.6 References......Page 186
7.1 Introduction......Page 187
7.2.1 Binary decision diagrams (BDDs)......Page 189
The decomposition principle......Page 190
BDD construction......Page 191
BDD composition - the APPLY algorithm......Page 192
Variable ordering......Page 193
Applications and limitations of BDDs......Page 194
7.2.2 Beyond BDDs......Page 195
The decomposition principle......Page 197
Reduction rules......Page 198
The APPLY algorithms......Page 199
Boolean logic......Page 200
Applications to word-level verification......Page 201
Symbolic algebra methods......Page 203
7.4.2 Motivation......Page 204
7.4.3 The Taylor series expansion......Page 205
7.4.4 Reduction and normalization......Page 208
7.4.5 Canonicity of Taylor expansion diagrams......Page 210
7.4.6 Complexity of Taylor expansion diagrams......Page 211
7.4.7 Composition of Taylor expansion diagrams......Page 213
TED construction for RTL designs......Page 216
7.4.9 Implementation and experimental results......Page 218
Experimental set-up......Page 219
Array processing......Page 220
DSP computations......Page 221
7.4.10 Limitations of TED representation......Page 223
7.5 Represention of multiple-output functions over finite fields......Page 226
7.5.1 Previous work......Page 227
Finite fields......Page 228
Generation of finite fields......Page 229
Notation......Page 230
7.5.3 Graph-based representation......Page 231
Canonicity......Page 234
A reduction algorithm......Page 236
7.5.5 Variable reordering......Page 237
Algebraic operations......Page 239
7.5.7 Multiple-output functions in GF(N)......Page 241
7.5.8 Further node reduction......Page 242
7.5.9 Representing characteristic functions in GF(N)......Page 243
7.5.10 Evaluation of functions......Page 244
Comparison of evaluation times......Page 245
Performance......Page 247
Evaluation time......Page 250
7.7 References......Page 254
8.1 Introduction......Page 260
8.2.1 Propositional formulas and satisfiability......Page 261
8.2.1.1 Resolution......Page 262
8.2.2 Boolean circuits......Page 263
8.2.3 Linear inequalities over Boolean variables......Page 264
8.2.4 SAT algorithms......Page 265
8.2.4.1 CDCL SAT algorithms......Page 266
8.2.4.3 Preprocessing......Page 269
8.3 Extensions of SAT......Page 270
8.4.2 Automatic test-pattern generation......Page 271
8.4.3 Design debugging......Page 273
8.4.4 Bounded model checking......Page 274
8.4.5 Unbounded model checking......Page 276
8.7 References......Page 277
Index......Page 283