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 -