Verification Techniques for System-Level Design
Regular price
36.000 KD
inc. VAT
Couldn't load pickup availability
Table of contents
- Contentsv
- Acknowledgmentsix
- Chapter 1 Introduction1
- Chapter 2 Higher-Level Design Methodology and Associated Verification Problems5
- 2.1 Introduction5
- 2.2 Issues in High-Level Design6
- 2.3 C/C++-Based Design and Specification Languages12
- 2.3.1 SpecC Language14
- 2.3.2 The Semantics of par Statements18
- 2.3.3 Relationship with Simulation Time21
- 2.4 System-Level Design Methodology Based on C/C++-Based Design and Specification Languages24
- 2.5 Verification Problems in High-Level Designs28
- Chapter 3 Basic Technology for Formal Verification33
- 3.1 The Boolean Satisfiability Problem33
- 3.2 The DPLL Algorithm34
- 3.3 Enhancements to Modern SAT Solvers35
- 3.4 Capabilities of Modern SAT Solvers38
- 3.5 Binary Decision Diagrams38
- 3.5.1 Manipulation of BDDs42
- 3.5.2 Variants of BDDs43
- 3.6 Automatic Test Pattern Generation Engines44
- 3.6.1 Single Stuck-at Testing for Combinational Circuits45
- 3.6.2 Stuck-at Testing in Sequential Circuits48
- 3.7 SAT, BDD, and ATPG Engines for Validation49
- 3.8 Theorem-Proving and Decision Procedures49
- References54
- Chapter 4 Verification Algorithms for FSM Models57
- 4.1 Combinational Equivalence Checking57
- 4.1.1 Sequential Equivalence Checking as Combinational Equivalence Checking57
- 4.1.2 Latch Mapping Problem58
- 4.1.3 EC Based on Internal Equivalences61
- 4.1.4 Anatomy and Capabilities of Modern CEC Tools64
- 4.2 Model Checking66
- 4.2.1 Modeling Concurrent Systems66
- 4.2.2 Temporal Logics66
- 4.2.3 Types of Properties70
- 4.2.4 Basic Model-Checking Algorithms70
- 4.2.5 Symbolic Model Checking74
- 4.3 Semi-Formal Verification Techniques83
- 4.3.1 SAT-Based Bounded Model Checking83
- 4.3.2 Symbolic Simulation88
- 4.3.3 Enhancing Simulation Using Formal Methods91
- 4.4 Conclusion93
- References93
- Chapter 5 Static Checking of Higher-Level Design Descriptions101
- 5.1 Program Slicing102
- 5.1.1 System Dependence Graph104
- 5.1.2 Nodes and Edges104
- 5.1.3 Concurrency104
- 5.1.4 Synchronization on Concurrent Processes104
- 5.2 Checking Method and Its Implying Design Flow106
- 5.2.1 Basic Static Description Checking108
- 5.2.2 Improvement of Accuracy Using Conditions of Control Nodes115
- 5.3 Application of the Checking Methods to HW/SW Partitioning and Optimization129
- 5.4 Case Study132
- 5.4.1 MPEG2132
- 5.4.2 JPEG2000132
- 5.4.3 Experimental Results on Static Checking133
- References134
- Chapter 6 Equivalence Checking on Higher-Level Design Descriptions137
- 6.1 Introduction137
- 6.2 High-Level Design Flow from the Viewpoint of Equivalence Checking138
- 6.3 Symbolic Simulation for Equivalence Checking141
- 6.4 Equivalence-Checking Methods Based on the Identification of Differences between two Descriptions144
- 6.4.1 Identification of Differences between Two Descriptions147
- 6.4.2 Symbolic Simulation Based on Textual Differences148
- 6.4.3 Example150
- 6.4.4 Experimental Results151
- 6.5 Further Improvement on the Use of Differences between Two Descriptions155
- 6.5.1 Extension of the Verification Area158
- 6.5.2 Symbolic Simulation on SDGs159
- 6.5.3 Verification Example159
- 6.5.4 Discussion of the Strategy of Extension160
- 6.5.5 Experimental Results on the Extension-Based Method160
- References162
- Chapter 7 Model Checking on Higher-Level Design Descriptions163
- 7.1 Introduction163
- 7.2 Goal of Synchronization Verification in High-Level Designs164
- 7.3 Model Checking and High-Level Design Descriptions167
- 7.4 Brief Review of SpecC and Its Semantics for Synchronization Verification168
- 7.5 Synchronization Verification Framework173
- 7.5.1 From SpecC to Boolean SpecC175
- 7.5.2 From Boolean SpecC to Mathematical Representations of Equalities/Inequalities176
- 7.5.3 Verification Method177
- 7.5.4 Validating the Abstract Counterexample179
- 7.5.5 Checking for Race Conditions179
- 7.5.6 Renaming Variables180
- 7.5.7 Predicate Discovery and Boolean SpecC Refinement180
- 7.6 Experimental Results181
- References185
- Chapter 8 Simulation-Based Verification Techniques for System-Level Designs187
- 8.1 Introduction187
- 8.2 Simulation Types188
- 8.2.1 Event-Driven Simulation189
- 8.2.2 Cycle-Based Simulation190
- 8.2.3 Specification/Behavior-Level Simulation191
- 8.2.4 Mixed-Mode Simulation191
- 8.3 High-Level Simulation Tools193
- 8.3.1 Static Checking (Linting)193
- 8.3.2 Simulators, Waveform Viewers, and Debuggers194
- 8.4 Simulation Drawbacks196
- 8.5 Coverage Metrics196
- 8.5.1 Drawbacks of Coverage Metrics202
- 8.6 Test-Bench Automation204
- 8.6.1 Transaction Level Modeling204
- 8.6.2 Property Specification Languages206
- 8.6.3 Test-Bench Automation Frameworks208
- 8.6.4 Model-Driven Automatic Test-Bench Generation209
- 8.6.5 Automatic Test-Bench Generation from Implementation Design212
- 8.7 Tackling Performance Issues213
- 8.7.1 Emulation and Hardware Acceleration214
- 8.7.2 Using Preverified IPs/Cores and Higher Abstraction Levels217
- 8.7.3 Correct by Construction Design218
- 8.8 Stopping Criteria219
- 8.9 An Example Case Study220
- 8.10 Conclusion228
- 8.11 Future Directions228
- References229
- Chapter 9 Conclusion231
- Index235
- A235
- B235
- C235
- D236
- E236
- F236
- H237
- I237
- J237
- K237
- L237
- M237
- N238
- O238
- P238
- Q238
- R238
- S239
- T240
- U240
- V240
- W240
- Z240
This book will explain how to verify SoC (Systems on Chip) logic designs using “formal and “semiformal verification techniques. The critical issue to be addressed is whether the functionality of the design is the one that the designers intended. Simulation has been used for checking the correctness of SoC designs (as in “functional verification), but many subtle design errors cannot be caught by simulation. Recently, formal verification, giving mathematical proof of the correctness of designs, has been gaining popularity.
For higher design productivity, it is essential to debug designs as early as possible, which this book facilitates. This book covers all aspects of high-level formal and semiformal verification techniques for system level designs.
• First book that covers all aspects of formal and semiformal, high-level (higher than RTL) design verification targeting SoC designs.
• Formal verification of high-level designs (RTL or higher).
• Verification techniques are discussed with associated system-level design methodology.
For higher design productivity, it is essential to debug designs as early as possible, which this book facilitates. This book covers all aspects of high-level formal and semiformal verification techniques for system level designs.
• First book that covers all aspects of formal and semiformal, high-level (higher than RTL) design verification targeting SoC designs.
• Formal verification of high-level designs (RTL or higher).
• Verification techniques are discussed with associated system-level design methodology.