QED and Symbolic QED: Dramatic Improvements in Pre-Silicon Verification and Post-Silicon Validation
By Keerthikumara Devarajegowda, Siemens EDA, Germany, keerthi.devraj@gmail.com | Florian Lonsing, Stanford University, USA | Mohammad R. Fadiheh, Stanford University, USA and Technische Universitaet Kaiserslautern, Germany | Saranyu Chattopadhyay, Stanford University, USA | David Lin, Stanford University, USA | Srinivas Shashank Nuthakki, Stanford University, USA | Eshan Singh, Stanford University, USA | Clark Barrett, Stanford University, USA | Wolfgang Ecker, Infineon Technologies AG, Germany | Wolfgang Kunz, Technische Universitaet Kaiserslautern, Germany | Yanjing Li, Stanford University, USA | Dominik Stoffel, Technische Universitaet Kaiserslautern, Germany | Subhasish Mitra, Stanford University, USA
Abstract
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. In an industrial case study using well-verified designs, Symbolic QED detected all logic bugs found by traditional methods and additional bugs they missed. This significantly boosted design productivity, reducing verification efforts by 8X for new designs and 80X for revisions. 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.
We also discuss Unique Program Execution Checking (UPEC), a hardware security verification technique inspired by QED principles. UPEC systematically detects Transient Execution Side-channels (TES) in processor implementations and has demonstrated its ability to detect Spectre and Meltdown type security attacks on complex processor cores, including out-of-order cores. UPEC is the first formal verification approach at the Register-Transfer Level that comprehensively checks for TES vulnerabilities in microarchitectures without prior knowledge of specific attacks. This enables the detection of new or previously unknown TES threats through UPEC rather than depending on the insights of security researchers and experts. Beyond the specific QED techniques described here, a new pre-silicon verification approach called G-QED (Generalized Quick Error Detection) is already demonstrating drastic benefits for pre-silicon verification of a wide variety of designs.
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.
