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-QED2). A-QED2 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-QED2; in particular, if the full HA under verification contains a bug, then A-QED2 ensures detection of that bug during A-QED verification of the corresponding sub-accelerators. Results on over 100 (buggy) versions of a wide variety of HAs with millions of logic gates demonstrate the effectiveness and practicality of A-QED2.
@article{arxiv.2108.06081,
title = {Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition},
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},
journal= {arXiv preprint arXiv:2108.06081},
year = {2022}
}
Comments
preprint of a paper to appear at FMCAD 2021, including appendix