Late Breaking Results: Towards Efficient Formal Verification of Dot Product Architectures
Lennart Weingarten, Kamalika Datta, Rolf Drechsler · 2025
The popularity of compute intensive applications, like AI/ML, has driven the design of processors with complex functionality. The Dot Product (DP) is one of the most essential operations in modern neural processors, although no complete formal verification technique exists that can ensure its 100% correctness. In this paper we show the first step towards formally verifying DP using Symbolic Computer Algebra (SCA). The verification process is performed without the need of a reference model generation which is a key factor in verification. Experimental results show the efficiency and scalability of SCA-based verification for DP architectures.