Stanford Seminar - QED and Symbolic QED- Dramatic Improvements in SoC Validation and Debug

This seminar presents Quick Error Detection (QED) for post-silicon validation and debug of complex system-on-chips, and Symbolic QED for formal bug detection and localization during pre- and post-silicon validation. It covers duplicate-and-check validation, coverage, error-detection latency, and bounded model checking, with results from commercial and open-source multicore SoCs.

Syllabus

Introduction.
Staggering IC Complexity.
Post-Silicon Validation Critical.
Post-Silicon Validation Difficult.
Scalability Barriers.
Bigger Obstacles at System Level.
Bug Example.
QED Example: Duplicate & Check Validation program.
QED Example: Duplicate & Check QED Trace.
QED Improves Coverage.
Diversity-Enhanced QED.
QED: Proactive Load & Check.
QED Coverage Considerations.
Error Detection Latency vs. Intrusiveness Improved error detection latency.
Intel® Core™ i7 Hardware.
8-Core QED: Difficult Logic Bugs.
8-Core QED: Power Management Bugs 100%.
Hybrid QED: Logic Bug Results.
Bug Localization.
Symbolic Quick Error Detection.
Traditional Bounded Model Checking.
BOUNDED MODEL CHECKING (BMC).
Traditional BMC vs. Symbolic QED.
BMC Challenge (1): Property.
Universal Property: QED Check.
QED Module.
QED Guarantees Quick Detection.
Partial Instantiation.