Verification Techniques for System-Level Design

by Fujita; Ghosh; Prasad

• ISBN13: 9780123706164
• ISBN10: 0123706165
• Format: Hardcover
• Copyright: 2007-10-17
• Publisher: Elsevier Science

Summary

The book presents readers with formal and semi-formal verification techniques for high-level design stages of LSI logic designs that drastically improve design productivity. High-level design support is the most critical issue in current digital system designs, and this book covers various aspects of verification issues that occur throughout design processes in C/C++ based languages.

Table of Contents

Acknowledgments	p. ix
Introduction	p. 1
Higher-Level Design Methodology and Associated Verification Problems	p. 5
Introduction	p. 5
Issues in High-Level Design	p. 6
C/C++-Based Design and Specification Languages	p. 12
SpecC Language	p. 14
The Semantics of par Statements	p. 18
Relationship with Simulation Time	p. 21
System-Level Design Methodology Based on C/C++-Based Design and Specification Languages	p. 24
Verification Problems in High-Level Designs	p. 28
Basic Technology for Formal Verification	p. 33
The Boolean Satisfiability Problem	p. 33
The DPLL Algorithm	p. 34
Enhancements to Modern SAT Solvers	p. 35
Capabilities of Modern SAT Solvers	p. 38
Binary Decision Diagrams	p. 38
Manipulation of BDDs	p. 42
Variants of BDDs	p. 43
Automatic Test Pattern Generation Engines	p. 44
Single Stuck-at Testing for Combinational Circuits	p. 45
Stuck-at Testing in Sequential Circuits	p. 48
SAT, BDD, and ATPG Engines for Validation	p. 49
Theorem-Proving and Decision Procedures	p. 49
References	p. 54
Verification Algorithms for FSM Models	p. 57
Combinational Equivalence Checking	p. 57
Sequential Equivalence Checking as Combinational Equivalence Checking	p. 57
Latch Mapping Problem	p. 58
EC Based on Internal Equivalences	p. 61
Anatomy and Capabilities of Modern CEC Tools	p. 64
Model Checking	p. 66
Modeling Concurrent Systems	p. 66
Temporal Logics	p. 66
Types of Properties	p. 70
Basic Model-Checking Algorithms	p. 70
Symbolic Model Checking	p. 74
Semi-Formal Verification Techniques	p. 83
SAT-Based Bounded Model Checking	p. 83
Symbolic Simulation	p. 88
Enhancing Simulation Using Formal Methods	p. 91
Conclusion	p. 93
References	p. 93
Static Checking of Higher-Level Design Descriptions	p. 101
Program Slicing	p. 102
System Dependence Graph	p. 104
Nodes and Edges	p. 104
Concurrency	p. 104
Synchronization on Concurrent Processes	p. 104
Checking Method and Its Implying Design Flow	p. 106
Basic Static Description Checking	p. 108
Improvement of Accuracy Using Conditions of Control Nodes	p. 115
Application of the Checking Methods to HW/SW Partitioning and Optimization	p. 129
Case Study	p. 132
MPEG2	p. 132
JPEG2000	p. 132
Experimental Results on Static Checking	p. 133
References	p. 134
Equivalence Checking on Higher-Level Design Descriptions	p. 137
Introduction	p. 137
High-Level Design Flow from the Viewpoint of Equivalence Checking	p. 138
Symbolic Simulation for Equivalence Checking	p. 141
Equivalence-Checking Methods Based on the Identification of Differences between two Descriptions	p. 144
Identification of Differences between Two Descriptions	p. 147
Symbolic Simulation Based on Textual Differences	p. 148
Example	p. 150
Experimental Results	p. 151
Further Improvement on the Use of Differences between Two Descriptions	p. 155
Extension of the Verification Area	p. 158
Symbolic Simulation on SDGs	p. 159
Verification Example	p. 159
Discussion of the Strategy of Extension	p. 160
Experimental Results on the Extension-Based Method	p. 160
References	p. 162
Model Checking on Higher-Level Design Descriptions	p. 163
Introduction	p. 163
Goat of Synchronization Verification in High-Level Designs	p. 164
Model Checking and High-Level Design Descriptions	p. 167
Brief Review of SpecC and Its Semantics for Synchronization Verification	p. 168
Synchronization Verification Framework	p. 173
From SpecC to Boolean SpecC	p. 175
From Boolean SpecC to Mathematical Representations of Equalities/Inequalities	p. 176
Verification Method	p. 177
Validating the Abstract Counterexample	p. 179
Checking for Race Conditions	p. 179
Renaming Variables	p. 180
Predicate Discovery and Boolean SpecC Refinement	p. 180
Experimental Results	p. 181
References	p. 185
Simulation-Based Verification Techniques for System-Level Designs	p. 187
Introduction	p. 187
Simulation Types	p. 188
Event-Driven Simulation	p. 189
Cycle-Based Simulation	p. 190
Specification/Behavior-Level Simulation	p. 191
Mixed-Mode Simulation	p. 191
High-Level Simulation Tools	p. 193
Static Checking (Linting)	p. 193
Simulators, Waveform Viewers, and Debuggers	p. 194
Simulation Drawbacks	p. 196
Coverage Metrics	p. 196
Drawbacks of Coverage Metrics	p. 202
Test-Bench Automation	p. 204
Transaction Level Modeling	p. 204
Property Specification Languages	p. 206
Test-Bench Automation Frameworks	p. 208
Model-Driven Automatic Test-Bench Generation	p. 209
Automatic Test-Bench Generation from Implementation Design	p. 212
Tackling Performance Issues	p. 213
Emulation and Hardware Acceleration	p. 214
Using Preverified IPs/Cores and Higher Abstraction Levels	p. 217
Correct by Construction Design	p. 218
Stopping Criteria	p. 219
An Example Case Study	p. 220
Conclusion	p. 228
Future Directions	p. 228
References	p. 229
Conclusion	p. 231
Index	p. 235
Table of Contents provided by Ingram. All Rights Reserved.