Publication

A Conflict-Aware Learning Approach to SCA Verification for MAC Architectures

Jan Kleinekathöfer; Lennart Weingarten; Kamalika Datta; Rolf Drechsler

In: Proceedings of the 33rd IEEE International Symposium on Computer Arithmetic. IEEE International Symposium on Computer Arithmetic (ARITH-2026), June 28 - July 1, Fulda, Germany, IEEE, 2026.

Abstract

Digital circuit verification remains an important area of research. To address this, various proof engines like Boolean Satisfiability (SAT), Binary Decision Diagrams (BDD), Answer Set Programming (ASP), and Symbolic Computer Algebra (SCA) have been explored. For specific complex circuits such as multipliers, Multiply and Accumulate (MAC) units, and Dot- Products, SCA has shown promise in the verification process. However, a major issue with SCA is the intermediate term explosion that can occur during verification. In this work, we design an SCA-based proof engine that exploits a conflict-aware learning approach. Together with dynamic ordering strategies and node polarity this compresses the intermediate polynomial expression, which significantly reduces the problem of term explosion. The approach introduces a preprocessing step that identifies and learns conflicts from the circuit structure and applies this knowledge during the verification to reduce polynomial size. We demonstrate the importance of each technique and specifically show how our proposed conflict optimization impacts the verification outcome.We experimentally validate the effectiveness of this approach by comparing our results with a state-of-the-art SCA-based proof engine using optimized MAC and other MAC architectures. The results demonstrate that the proposed method successfully verifies circuits that remained unverifiable using previous approaches.