QED and Symbolic QED: Dramatic Improvements in Pre-Silicon Verification and Post-Silicon Validation
Bibliographic record
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 presilicon 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.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.006 | 0.014 |
| Meta-epidemiology (narrow) | 0.002 | 0.002 |
| Meta-epidemiology (broad) | 0.001 | 0.002 |
| Bibliometrics | 0.002 | 0.001 |
| Science and technology studies | 0.001 | 0.003 |
| Scholarly communication | 0.003 | 0.007 |
| Open science | 0.003 | 0.003 |
| Research integrity | 0.002 | 0.005 |
| Insufficient payload (model declined to judge) | 0.014 | 0.005 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".