QED and Symbolic QED: Dramatic Improvements in Pre-Silicon Verification and Post-Silicon Validation

System-on-Chips (SoCs) are an integral part of our lives. The complexity of SoCs requires sophisticated tools and methods for ensuring functional correctness, especially in critical domains such as automotive and healthcare applications. In addition, the prevalence of security features in SoCs and emerging threats such as Spectre and Meltdown underscore the need for advanced verification techniques to combat security vulnerabilities. Existing verification approaches consume over 50% of development effort. Pre-silicon verification ensures functional correctness before chip fabrication, while post-silicon validation detects bugs that escape pre-silicon verification. Existing pre-silicon and post-silicon approaches are inadequate resulting in skyrocketing bug escapes and respins. To address these challenges, this book presents pre-silicon verification and post-silicon validation methods based on Quick Error Detection (QED) principles: self-consistency checking to detect and localize design bugs. Symbolic QED combines QED principles with model checking (a formal verification technique) for pre-silicon verification. Many studies, including industrial case studies, have demonstrated the effectiveness and practicality of Symbolic QED. QED-based methods for post-silicon validation significantly reduce the error detection latency (the time elapsed between the occurrence of a bug and its manifestation as an observable failure) by several orders of magnitude, addressing the limitations of existing validation and debug approaches. This book also discusses Unique Program Execution Checking (UPEC), a hardware security verification technique inspired by QED principles. Beyond the specific QED techniques described here, a new pre-silicon verification approach called G-QED (Generalized Quick Error Detection) is already demonstrating significant drastic benefits for pre-silicon verification of a wide variety of designs. See more