Publication
Late Breaking Results: Efficient Formal Verification of Highly Optimized MAC Units
Jan Kleinekathöfer; Lennart Weingarten; Kamalika Datta; Rolf Drechsler
In: Design, Automation and Test in Europe Conference (DATE). Design, Automation & Test in Europe (DATE-2026), April 20-22, Verona, Italy, 2026.
Abstract
The demand for compute-intensive applications such as AI/ML has led to the development of processors with complex functionalities. The Multiply Accumulate (MAC) unit is a vital
component in these processors, but its verification is very challenging due to the highly optimized designs used to implement the MAC operation. In this paper, we show some interesting results for optimized MAC design verification using a formal proof engine, Symbolic Computer Algebra (SCA). For the first time, we exploit the combined benefit of phase and dynamic ordering in verifying MAC circuits, a capability not possible using state-of-the-art SCA proof engines.