AI 中文总结
针对AI时代算术原语验证的计算瓶颈，提出SCA框架TRACE，采用优化归约技术，首次成功验证此前无法验证的优化MAC电路。
AI 中文摘要
复杂电路的现代硬件验证高度依赖形式化方法的效率，尤其是针对复杂算术电路，采用多项式表示伪布尔函数的符号计算机代数（Symbolic Computer Algebra, SCA）引擎至关重要。随着AI时代电路复杂度不断提升，乘法、加法、乘累加（Multiply-Accumulate, MAC）等算术原语的验证成为计算瓶颈。为解决该问题，本文提出TRACE（Traversal and Reasoning Algebraic Computing Engine，遍历与推理代数计算引擎），这是一款高效框架，旨在研究遍历策略与证明效率的交叉领域。与现有主要局限于乘法器的SCA工具不同，TRACE为研究人员提供灵活框架，可分析加法器、乘法器、MAC等各类算术电路的内存占用与验证时间。为克服多项式展开固有的状态爆炸问题，该引擎采用高级归约技术，包括优化的遍历策略、冲突消除及基于极性的优化，以实现紧凑的符号表示。实验结果表明，针对优化后的MAC，TRACE首次成功验证了此前无法验证的电路。
英文摘要
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
