“QED and Symbolic QED: Dramatic Improvements in Pre-Silicon Verification and Post-Silicon Validation” by Keerthikumara Devarajegowda, Florian Lonsing, Mohammad R. Fadiheh, Saranyu Chattopadhyay, David Lin, Srinivas Shashank Nuthakki, Eshan Singh, Clark Barrett, Wolfgang Ecker, Wolfgang Kunz, Yanjing Li, Dominik Stoffel, and Subhasish Mitra. Foundations and Trends in Integrated Circuits and Systems, vol. 3, no. 2--3, Oct. 2024, pp. 51-217, now publishers inc..
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.
BibTeX entry:
@article{DLF+24,
author = {Keerthikumara Devarajegowda and Florian Lonsing and Mohammad
R. Fadiheh and Saranyu Chattopadhyay and David Lin and Srinivas
Shashank Nuthakki and Eshan Singh and Clark Barrett and Wolfgang
Ecker and Wolfgang Kunz and Yanjing Li and Dominik Stoffel and
Subhasish Mitra},
title = {{QED} and Symbolic {QED}: Dramatic Improvements in Pre-Silicon
Verification and Post-Silicon Validation},
journal = {Foundations and Trends in Integrated Circuits and Systems},
volume = {3},
number = {2--3},
pages = {51--217},
publisher = {now publishers inc.},
month = oct,
year = {2024},
doi = {10.1561/3500000003},
url = {http://dx.doi.org/10.1561/3500000003}
}
(This webpage was created with bibtex2web.)