Publikation
ForMAt: Formal Verification of Scalable Multiply and Accumulate Units
Lennart Weingarten; Kamalika Datta; Rolf Drechsler
In: Forum on specification & Design Languages (FDL). Forum on Specification & Design Languages (FDL), September 10-12, St. Goar, Germany, 2025.
Zusammenfassung
With the increasing popularity of compute intensive
applications like AI, processors with complex functionalities are
designed. Multiply and Accumulate (MAC) is one of the essential
operations in modern Neural Processor Units (NPUs), but no
sound formal verification technique exists that can efficiently
ensure correctness. In this paper we analyze almost 200 configurations of MAC instances for various bit-widths starting from
8 up to several hundred bits. On top of the classical area-delay
trade-off, we study verifiability as an additional parameter. It
is shown that surprisingly the fastest and smallest instances are
not the ones that are the hardest to verify. Exploiting Symbolic
Computer Algebra (SCA) we provide a technique that allows
scalable verification for large bit-width and classifies the set of
MAC units