Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition

TL;DR

This paper introduces A-QED$^2$, a scalable verification method for hardware accelerators that decomposes large designs into smaller modules, enabling effective bug detection with formal methods.

Contribution

The paper presents a novel decomposition technique for A-QED, called A-QED$^2$, which improves scalability by verifying smaller sub-modules independently while maintaining completeness.

Findings

Successfully verified over 100 buggy hardware accelerators.

Demonstrated effectiveness on designs with millions of logic gates.

Proved completeness of the decomposition-based verification approach.

Abstract

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 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-QED$^2$.