TY - GEN
T1 - G-QED
T2 - 60th ACM/IEEE Design Automation Conference, DAC 2023
AU - Chattopadhyay, Saranyu
AU - Devarajegowda, Keerthikumara
AU - Zhao, Bihan
AU - Lonsing, Florian
AU - D'Agostino, Brandon A.
AU - Vavelidou, Ioanna
AU - Bhatt, Vijay D.
AU - Prebeck, Sebastian
AU - Ecker, Wolfgang
AU - Trippel, Caroline
AU - Barrett, Clark
AU - Mitra, Subhasish
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023
Y1 - 2023
N2 - Hardware accelerators (HAs) underpin high-performance and energy-efficient digital systems. Correctness of these systems thus depends on the correctness of constituent HAs. Self-consistency-based pre-silicon verification techniques, like A-QED (Accelerator Quick Error Detection), provide a quick and provably thorough HA verification framework that does not require extensive design-specific properties or a full functional specification. However, A-QED is limited to verifying HAs which are non-interfering - i.e., they produce the same result for a given input independent of its context within a sequence of inputs. We present a new technique called G-QED (Generalized QED) which goes beyond non-interfering HAs while retaining A-QED's benefits. Our extensive results as well as a detailed industrial case study show that: G-QED is highly thorough in detecting critical bugs in well-verified designs that otherwise escape traditional verification flows while simultaneously improving verification productivity 18-fold (from 370 person days to 21 person days). These results are backed by theoretical guarantees of soundness and completeness.
AB - Hardware accelerators (HAs) underpin high-performance and energy-efficient digital systems. Correctness of these systems thus depends on the correctness of constituent HAs. Self-consistency-based pre-silicon verification techniques, like A-QED (Accelerator Quick Error Detection), provide a quick and provably thorough HA verification framework that does not require extensive design-specific properties or a full functional specification. However, A-QED is limited to verifying HAs which are non-interfering - i.e., they produce the same result for a given input independent of its context within a sequence of inputs. We present a new technique called G-QED (Generalized QED) which goes beyond non-interfering HAs while retaining A-QED's benefits. Our extensive results as well as a detailed industrial case study show that: G-QED is highly thorough in detecting critical bugs in well-verified designs that otherwise escape traditional verification flows while simultaneously improving verification productivity 18-fold (from 370 person days to 21 person days). These results are backed by theoretical guarantees of soundness and completeness.
KW - Accelerators
KW - Functional consistency
KW - Processors
KW - QED
KW - Quick Error Detection
UR - http://www.scopus.com/inward/record.url?scp=85173125942&partnerID=8YFLogxK
U2 - 10.1109/DAC56929.2023.10247903
DO - 10.1109/DAC56929.2023.10247903
M3 - Conference contribution
AN - SCOPUS:85173125942
T3 - Proceedings - Design Automation Conference
BT - 2023 60th ACM/IEEE Design Automation Conference, DAC 2023
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 9 July 2023 through 13 July 2023
ER -