TRACE: Traversal and Reasoning Algebraic Computing Engine for Formal Hardware Verification
2026-08-17 • Hardware Architecture
Hardware Architecture
AI summaryⓘ
The authors developed TRACE, a new tool to help check if complex math circuits like adders, multipliers, and multiply-accumulators (MAC) work correctly. Current methods struggle with these tasks because the math involved gets too big and complicated. TRACE uses smarter ways to explore the problem and simplify the math, making verification faster and using less memory. Their tests show TRACE can verify some multiply-accumulate circuits that were too hard to check before.
formal methodshardware verificationarithmetic circuitssymbolic computer algebrapseudo-boolean functionspolynomial expansionmultiplicationadder circuitsmultiply-accumulate (MAC)state-explosion problem
Authors
Jan Kleinekathöfer, Lennart Weingarten, Kamalika Datta, Rolf Drechsler
Abstract
Modern hardware verification of complex circuits relies heavily on the efficiency of formal methods. For complex arithmetic circuits in particular Symbolic Computer Algebra (SCA) engines which represent pseudo-boolean functions using polynomials are crucial. As circuit complexity grows in the age of AI, verification of arithmetic primitives, including Multiplication, Addition, Multiply-Accumulate (MAC), becomes a computational bottleneck. To address this, we introduce TRACE (Traversal and Reasoning Algebraic Computing Engine), a highly efficient framework designed to investigate the intersection of traversal strategies and proof efficiency. Unlike existing SCA tools which are mainly limited to multipliers, TRACE offers a flexible framework for researchers to analyze memory usage and verification time across a wide range of arithmetic circuits (adder, multiplier and MAC). To overcome the state-explosion problem inherent in polynomial expansion, the engine incorporates advanced reduction techniques, including optimized traversal strategies, conflict removal, and polarity-based optimization for compact symbolic representations. Our experimental results show that for optimized MAC, for the first time, TRACE was able to verify previously unverifiable circuits