Verification Techniques for System-Level Design (eBook)

Front Cover 1
Verification Techniques For System-Level Design 4
Copyright Page 5
Contents 6
Acknowledgments 10
Chapter 1 Introduction 12
Chapter 2 Higher-Level Design Methodology and Associated Verification Problems 16
2.1 Introduction 16
2.2 Issues in High-Level Design 17
2.3 C/C++-Based Design and Specification Languages 23
2.3.1 SpecC Language 25
2.3.2 The Semantics of par Statements 29
2.3.3 Relationship with Simulation Time 32
2.4 System-Level Design Methodology Based on C/C++-Based Design and Specification Languages 35
2.5 Verification Problems in High-Level Designs 39
Chapter 3 Basic Technology for Formal Verification 44
3.1 The Boolean Satisfiability Problem 44
3.2 The DPLL Algorithm 45
3.3 Enhancements to Modern SAT Solvers 46
3.4 Capabilities of Modern SAT Solvers 49
3.5 Binary Decision Diagrams 49
3.5.1 Manipulation of BDDs 53
3.5.2 Variants of BDDs 54
3.6 Automatic Test Pattern Generation Engines 55
3.6.1 Single Stuck-at Testing for Combinational Circuits 56
3.6.2 Stuck-at Testing in Sequential Circuits 59
3.7 SAT, BDD, and ATPG Engines for Validation 60
3.8 Theorem-Proving and Decision Procedures 60
References 65
Chapter 4 Verification Algorithms for FSM Models 68
4.1 Combinational Equivalence Checking 68
4.1.1 Sequential Equivalence Checking as Combinational Equivalence Checking 68
4.1.2 Latch Mapping Problem 69
4.1.3 EC Based on Internal Equivalences 72
4.1.4 Anatomy and Capabilities of Modern CEC Tools 75
4.2 Model Checking 77
4.2.1 Modeling Concurrent Systems 77
4.2.2 Temporal Logics 77
4.2.3 Types of Properties 81
4.2.4 Basic Model-Checking Algorithms 81
4.2.5 Symbolic Model Checking 85
4.3 Semi-Formal Verification Techniques 94
4.3.1 SAT-Based Bounded Model Checking 94
4.3.2 Symbolic Simulation 99
4.3.3 Enhancing Simulation Using Formal Methods 102
4.4 Conclusion 104
References 104
Chapter 5 Static Checking of Higher-Level Design Descriptions 112
5.1 Program Slicing 113
5.1.1 System Dependence Graph 115
5.1.2 Nodes and Edges 115
5.1.3 Concurrency 115
5.1.4 Synchronization on Concurrent Processes 115
5.2 Checking Method and Its Implying Design Flow 117
5.2.1 Basic Static Description Checking 119
5.2.2 Improvement of Accuracy Using Conditions of Control Nodes 126
5.3 Application of the Checking Methods to HW/SW Partitioning and Optimization 140
5.4 Case Study 143
5.4.1 MPEG2 143
5.4.2 JPEG2000 143
5.4.3 Experimental Results on Static Checking 144
References 145
Chapter 6 Equivalence Checking on Higher-Level Design Descriptions 148
6.1 Introduction 148
6.2 High-Level Design Flow from the Viewpoint of Equivalence Checking 149
6.3 Symbolic Simulation for Equivalence Checking 152
6.4 Equivalence-Checking Methods Based on the Identification of Differences between two Descriptions 155
6.4.1 Identification of Differences between Two Descriptions 158
6.4.2 Symbolic Simulation Based on Textual Differences 159
6.4.3 Example 161
6.4.4 Experimental Results 162
6.5 Further Improvement on the Use of Differences between Two Descriptions 166
6.5.1 Extension of the Verification Area 169
6.5.2 Symbolic Simulation on SDGs 170
6.5.3 Verification Example 170
6.5.4 Discussion of the Strategy of Extension 171
6.5.5 Experimental Results on the Extension-Based Method 171
References 173
Chapter 7 Model Checking on Higher-Level Design Descriptions 174
7.1 Introduction 174
7.2 Goal of Synchronization Verification in High-Level Designs 175
7.3 Model Checking and High-Level Design Descriptions 178
7.4 Brief Review of SpecC and Its Semantics for Synchronization Verification 179
7.5 Synchronization Verification Framework 184
7.5.1 From SpecC to Boolean SpecC 186
7.5.2 From Boolean SpecC to Mathematical Representations of Equalities/Inequalities 187
7.5.3 Verification Method 188
7.5.4 Validating the Abstract Counterexample 190
7.5.5 Checking for Race Conditions 190
7.5.6 Renaming Variables 191
7.5.7 Predicate Discovery and Boolean SpecC Refinement 191
7.6 Experimental Results 192
References 196
Chapter 8 Simulation-Based Verification Techniques for System-Level Designs 198
8.1 Introduction 198
8.2 Simulation Types 199
8.2.1 Event-Driven Simulation 200
8.2.2 Cycle-Based Simulation 201
8.2.3 Specification/Behavior-Level Simulation 202
8.2.4 Mixed-Mode Simulation 202
8.3 High-Level Simulation Tools 204
8.3.1 Static Checking (Linting) 204
8.3.2 Simulators, Waveform Viewers, and Debuggers 205
8.4 Simulation Drawbacks 207
8.5 Coverage Metrics 207
8.5.1 Drawbacks of Coverage Metrics 213
8.6 Test-Bench Automation 215
8.6.1 Transaction Level Modeling 215
8.6.2 Property Specification Languages 217
8.6.3 Test-Bench Automation Frameworks 219
8.6.4 Model-Driven Automatic Test-Bench Generation 220
8.6.5 Automatic Test-Bench Generation from Implementation Design 223
8.7 Tackling Performance Issues 224
8.7.1 Emulation and Hardware Acceleration 225
8.7.2 Using Preverified IPs/Cores and Higher Abstraction Levels 228
8.7.3 Correct by Construction Design 229
8.8 Stopping Criteria 230
8.9 An Example Case Study 231
8.10 Conclusion 239
8.11 Future Directions 239
References 240
Chapter 9 Conclusion 242
Index 246
A 246
B 246
C 246
D 247
E 247
F 247
H 248
I 248
J 248
K 248
L 248
M 248
N 249
O 249
P 249
Q 249
R 249
S 250
T 251
U 251
V 251
W 251
Z 251