TY - GEN
T1 - Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
AU - Chattopadhyay, Saranyu
AU - Lonsing, Florian
AU - Piccolboni, Luca
AU - Soni, Deepraj
AU - Wei, Peng
AU - Zhang, Xiaofan
AU - Zhou, Yuan
AU - Carloni, Luca
AU - Chen, Deming
AU - Cong, Jason
AU - Karri, Ramesh
AU - Zhang, Zhiru
AU - Trippel, Caroline
AU - Barrett, Clark
AU - Mitra, Subhasish
N1 - Publisher Copyright:
© 2021 FMCAD Associ.
PY - 2021
Y1 - 2021
N2 - 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-Q E D2). 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-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 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-QED2.
AB - 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-Q E D2). 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-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 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-QED2.
UR - http://www.scopus.com/inward/record.url?scp=85123726481&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85123726481&partnerID=8YFLogxK
U2 - 10.34727/2021/isbn.978-3-85448-046-4_12
DO - 10.34727/2021/isbn.978-3-85448-046-4_12
M3 - Conference contribution
AN - SCOPUS:85123726481
T3 - Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021
SP - 42
EP - 52
BT - Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021
A2 - Piskac, Ruzica
A2 - Whalen, Michael W.
A2 - Hunt, Warren A.
A2 - Weissenbacher, Georg
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 21st International Conference on Formal Methods in Computer-Aided Design, FMCAD 2021
Y2 - 18 October 2021 through 22 October 2021
ER -