A-QED Verification of Hardware Accelerators

A-QED Verification of Hardware Accelerators” by Eshan Singh, Florian Lonsing, Saranyu Chattopadhyay, Max Strange, Peng Wei, Xiaofan Zhang, Yuan Zhao, Jason Cong, Deming Chen, Zhiru Zhang, Priyankja Raina, Clark Barrett, and Subhasish Mitra. In Proceedings of the 57^th Design Automation Conference (DAC '20), July 2020.

Abstract

We present A-QED (Accelerator-Quick Error Detection), a new approach for pre-silicon formal verification of stand-alone hardware accelerators. A-QED relies on bounded model checking -- however, it does not require extensive design-specific properties or a full formal design specification. While A- QED is effective for both RTL and high-level synthesis (HLS) design flows, it integrates seamlessly with HLS flows. Our A-QED results on several hardware accelerator designs demonstrate its practicality and effectiveness: 1. A-QED detected all bugs detected by conventional verification flow. 2. A-QED detected bugs that escaped conventional verification flow. 3. A-QED improved verification productivity dramatically, by 30X, in one of our case studies (1 person-day using A-QED vs. 30 person-days using conventional verification flow). 4. A-QED produced short counterexamples for easy debug (37X shorter on average vs. conventional verification flow).

BibTeX entry:

@inproceedings{SLC+20,
   author = {Eshan Singh and Florian Lonsing and Saranyu Chattopadhyay and
	Max Strange and Peng Wei and Xiaofan Zhang and Yuan Zhao and Jason
	Cong and Deming Chen and Zhiru Zhang and Priyankja Raina and Clark
	Barrett and Subhasish Mitra},
   title = {{A-QED} Verification of Hardware Accelerators},
   booktitle = {Proceedings of the {\it 57^{th}} Design Automation
	Conference (DAC '20)},
   publisher = {Association for Computing Machinery},
   month = jul,
   year = {2020},
   doi = {10.1109/DAC18072.2020.9218715},
   url = {http://theory.stanford.edu/~barrett/pubs/SLC+20.pdf}
}

(This webpage was created with bibtex2web.)