“Scaling Up
Hardware Accelerator Verification using A-QED with Functional
Decomposition”
by Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark Barrett, and Subhasish Mitra.
In *Proceedings of the 21^st International Conference on Formal
Methods In Computer-Aided Design (FMCAD '21)*, (Ruzica Piskac and
Michael W. Whalen, eds.), Oct. 2021, pp. 42-52.

Hardware accelerators (HAs) are essential building blocks for fast and
energy-efficient computing systems. Accelerator Quick Error Detection
(A-QED) is a recent formal technique which uses Bounded Model Checking for
pre-silicon verification of HAs. A-QED checks an HA for self-consistency,
i.e., whether identical inputs within a sequence of operations always
produce the same output. Under modest assumptions, A-QED is both sound and
complete. However, as is well-known, large design sizes significantly
limit the scalability of formal verification, including A-QED. We overcome
this scalability challenge through a new decomposition technique for
A-QED, called A-QED with Decomposition (A-QED*^2*). A-QED*^2*
systematically decomposes an HA into smaller, functional sub-modules,
called sub-accelerators, which are then verified independently using
A-QED. We prove completeness of A-QED*^2* ; in particular, if the
full HA under verification contains a bug, then A-QED*^2* ensures
detection of that bug during A-QED verification of the corresponding
subaccelerators. Results on over 100 (buggy) versions of a wide variety of
HAs with millions of logic gates demonstrate the effectiveness and
practicality of A-QED*^2*.

**BibTeX entry:**

@inproceedings{CLP+21, author = {Saranyu Chattopadhyay and Florian Lonsing and Luca Piccolboni and Deepraj Soni and Peng Wei and Xiaofan Zhang and Yuan Zhou and Luca Carloni and Deming Chen and Jason Cong and Ramesh Karri and Zhiru Zhang and Caroline Trippel and Clark Barrett and Subhasish Mitra}, editor = {Ruzica Piskac and Michael W. Whalen}, title = {Scaling Up Hardware Accelerator Verification using {A-QED} with Functional Decomposition}, booktitle = {Proceedings of the {\it 21^{st}} International Conference on Formal Methods In Computer-Aided Design (FMCAD '21)}, pages = {42--52}, publisher = {TU Wien Academic Press}, month = oct, year = {2021}, doi = {10.34727/2021/isbn.978-3-85448-046-4_12}, url = {http://theory.stanford.edu/~barrett/pubs/CLP+21.pdf} }

(This webpage was created with bibtex2web.)