G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators

G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators” by Saranyu Chattopadhyay, Keerthikumara Devarajegowda, Bihan Zhao, Florian Lonsing, Brandon A. D'Agostino, Ioanna Vavelidou, Vijay D. Bhatt, Sebastian Prebeck, Wolfgang Ecker, Caroline Trippel, Clark Barrett, and Subhasish Mitra. In Proceedings of the 60^th Design Automation Conference (DAC '23), July 2023. San Francisco, CA.

Abstract

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.

Keywords: Productivity; Context; Design automation; Digital systems; Side-channel attacks; Energy efficiency; Timing; QED; Quick Error Detection; Accelerators; Processors; Functional consistency

BibTeX entry:

@inproceedings{CDZ+23,
   author = {Saranyu Chattopadhyay and Keerthikumara Devarajegowda and
	Bihan Zhao and Florian Lonsing and Brandon A. D'Agostino and
	Ioanna Vavelidou and Vijay D. Bhatt and Sebastian Prebeck and
	Wolfgang Ecker and Caroline Trippel and Clark Barrett and
	Subhasish Mitra},
   title = {{G-QED}: Generalized {QED} Pre-silicon Verification beyond
	Non-Interfering Hardware Accelerators},
   booktitle = {Proceedings of the {\it 60^{th}} Design Automation
	Conference (DAC '23)},
   publisher = {IEEE},
   month = jul,
   year = {2023},
   doi = {10.1109/DAC56929.2023.10247903},
   note = {San Francisco, CA},
   url = {https://ieeexplore.ieee.org/document/10247903}
}

(This webpage was created with bibtex2web.)