“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.)