| Introduction | p. 1 |
| Growing SoC Validation Complexity | p. 1 |
| System-Level Validation: Opportunities and Challenges | p. 3 |
| Top-Down Design and Validation Flow | p. 4 |
| SoC Validation Approaches | p. 6 |
| Opportunities in System-Level Validation | p. 10 |
| System-Level Validation Challenges | p. 12 |
| A Comprehensive Approach for System-Level Validation | p. 14 |
| Book Organization | p. 14 |
| References | p. 15 |
| Modeling and Specification of SoC Designs | p. 19 |
| Introduction | p. 19 |
| Modeling of Complex Systems | p. 19 |
| Graph-Based Modeling | p. 20 |
| FSM-Based Behavior Modeling | p. 20 |
| Specification Using SystemC TLMs | p. 22 |
| Modeling of SystemC TLM Designs | p. 22 |
| Transformation from SystemC TLM to SMV | p. 24 |
| Case Study: A Router Example | p. 28 |
| Specification Using UML Activity Diagrams | p. 29 |
| Graphic Notations | p. 30 |
| Formal Modeling of UML Activity Diagrams | p. 32 |
| Transformation from UML Activity Diagrams to SMV | p. 36 |
| Case Study: A Stock Exchange System | p. 40 |
| Chapter Summary | p. 40 |
| References | p. 40 |
| Automated Generation of Directed Tests | p. 43 |
| Introduction | p. 43 |
| Related Work | p. 44 |
| The Workflow of Model Checking Based Test Generation | p. 45 |
| Coverage-Driven Property Generation | p. 46 |
| Safety Property and Its Negation | p. 46 |
| Testing Adequacy Using Model Checking | p. 48 |
| Fault Models | p. 48 |
| Functional Coverage Based on Fault Models | p. 51 |
| Test Generation Using Model Checking Techniques | p. 51 |
| Test Generation Using Unbounded Model Checking | p. 51 |
| Test Generation Using Bounded Model Checking | p. 52 |
| Case Studies | p. 54 |
| A Control System | p. 55 |
| A Stock Exchange System | p. 56 |
| Chapter Summary | p. 57 |
| References | p. 58 |
| Functional Test Compaction | p. 61 |
| Introduction | p. 61 |
| Manufacturing Test Reduction Techniques | p. 61 |
| Test Compression | p. 63 |
| Test Compaction | p. 63 |
| Applicability and Limitations | p. 65 |
| Functional Test Compaction | p. 67 |
| Binary Format of FSM Models | p. 68 |
| Number of FSM States and Transitions | p. 70 |
| Property Compaction of FSM States and Transitions | p. 71 |
| FSM Coverage-Driven Test Selection and Generation | p. 73 |
| A Case Study | p. 74 |
| Chapter Summary | p. 76 |
| References | p. 76 |
| Property Clustering and Learning Techniques | p. 79 |
| Introduction | p. 79 |
| Related Work | p. 80 |
| Background: SAT Solver Implementation | p. 81 |
| DPLL Algorithm | p. 81 |
| Conflict Clause | p. 82 |
| Property Clustering | p. 84 |
| Similarity Based on Structural Overlap | p. 85 |
| Similarity Based on Textual Overlap | p. 86 |
| Similarity Based on Influence | p. 87 |
| Similarity Based on CNF Intersection | p. 88 |
| Determination of Base Property | p. 88 |
| Conflict Clause Based Test Generation | p. 89 |
| Conflict Clause Forwarding Techniques | p. 89 |
| Name Substitution for Computation of Intersections | p. 91 |
| Identification and Reuse of Common Conflict Clauses | p. 92 |
| Case Studies | p. 93 |
| A MIPS Processor | p. 94 |
| A Stock Exchange System | p. 102 |
| Chapter Summary | p. 104 |
| References | p. 105 |
| Decision Ordering Based Learning Techniques | p. 107 |
| Introduction | p. 107 |
| Related Work | p. 108 |
| Decision Ordering Based Learnings | p. 108 |
| Motivation | p. 109 |
| Bit Value Ordering | p. 110 |
| Variable Ordering | p. 111 |
| Hybrid Learning from Conflict Clauses and Decision Ordering | p. 112 |
| Test Generation Using Decision Ordering Techniques | p. 113 |
| Test Generation for a Single Property | p. 114 |
| Test Generation for Similar Properties | p. 116 |
| Case Studies | p. 119 |
| Intra-Property Learning | p. 119 |
| Inter-Property Learning | p. 123 |
| Chapter Summary | p. 127 |
| References | p. 127 |
| Synchronized Generation of Directed Tests | p. 129 |
| Introduction | p. 129 |
| Related Work | p. 130 |
| Synchronized Test Generation | p. 130 |
| Correctness of STG | p. 135 |
| Implementation Details | p. 136 |
| Case Studies | p. 137 |
| A Stock Exchange System | p. 137 |
| A MIPS Processor | p. 140 |
| Chapter Summary | p. 142 |
| References | p. 142 |
| Test Generation Using Design and Property Decompositions | p. 145 |
| Introduction | p. 145 |
| Related Work | p. 147 |
| Decomposition of Design and Property | p. 148 |
| Design Decomposition | p. 149 |
| Property Decomposition | p. 150 |
| Decompositional Test Generation | p. 155 |
| Test Generation Using Module-Level Partitioning | p. 158 |
| Test Generation Using Path-Level Partitioning | p. 160 |
| Merging Partial Counterexamples | p. 161 |
| A Case Study | p. 162 |
| Module-Level Decomposition | p. 163 |
| Group-Level Decomposition Based on Time Step | p. 164 |
| Discussion: Applicability and Limitations | p. 166 |
| Chapter Summary | p. 166 |
| References | p. 166 |
| Learning-Oriented Property Decomposition Approaches | p. 169 |
| Introduction | p. 169 |
| Related Work | p. 170 |
| Learning-Oriented Property Decomposition | p. 171 |
| Spatial Property Decomposition | p. 171 |
| Temporal Property Decomposition | p. 174 |
| Decision Ordering Based Learning Techniques | p. 176 |
| Test Generation Using Decomposition and Learning Techniques | p. 178 |
| An Illustrative Example | p. 179 |
| Spatial Decomposition | p. 179 |
| Temporal Decomposition | p. 180 |
| Case Studies | p. 181 |
| A MIPS Processor | p. 181 |
| A Stock Exchange System | p. 182 |
| Chapter Summary | p. 183 |
| References | p. 184 |
| Directed Test Generation for Multicore Architectures | p. 185 |
| Introduction | p. 185 |
| Related Work | p. 186 |
| Test Generation for Multicore Architectures | p. 187 |
| Correctness of TGMA | p. 191 |
| Implementation Details | p. 193 |
| Heterogeneous Multicore Architectures | p. 194 |
| Case Studies | p. 195 |
| Experimental Setup | p. 195 |
| Results | p. 196 |
| Chapter Summary | p. 199 |
| References | p. 199 |
| Test Generation for Cache Coherence Validation | p. 201 |
| Introduction | p. 201 |
| Related Work | p. 202 |
| Background and Motivation | p. 203 |
| Test Generation for Transition Coverage | p. 204 |
| SI Protocol | p. 205 |
| MSI Protocol | p. 206 |
| MESI Protocol | p. 208 |
| MOSI Protocol | p. 209 |
| Case Studies | p. 210 |
| Chapter Summary | p. 213 |
| References | p. 213 |
| Reuse of System-Level Validation Efforts | p. 215 |
| Introduction | p. 215 |
| Related Work | p. 216 |
| RTL Test Generation from TLM Specifications | p. 217 |
| Automatic TLM Test Generation | p. 217 |
| Translation from TLM Tests to RTL Tests | p. 219 |
| A Prototype Tool for TLM-to-RTL Validation Refinement | p. 222 |
| Case Studies | p. 224 |
| A Router Example | p. 224 |
| A Pipelined Processor Example | p. 228 |
| Chapter Summary | p. 233 |
| References | p. 233 |
| Conclusions | p. 235 |
| Summary | p. 235 |
| Future Directions | p. 237 |
| Appendix A: Acknowledgments of Copyrighted Materials | p. 239 |
| Index | p. 243 |
| Table of Contents provided by Ingram. All Rights Reserved. |