Arisca：用于算术电路验证的参数化符号代数框架
Arisca: A Parameterized Symbolic Algebra Framework for Arithmetic Circuit Verification
AI总结：
针对门级算术电路验证难题，Arisca开源框架用符号计算机代数，建立广义参数空间统一技术，提出算法改进，扩展验证范围，在乘法器基准测试等中实现SOTA性能。
AI中文摘要：
由于状态空间爆炸问题，门级高度优化的算术电路的形式验证仍然是一项重大挑战。虽然符号计算机代数（SCA）通过将电路建模为多元多项式提供了可扩展的理论基础，但实际实现经常受到中间多项式大小爆炸的困扰。本文介绍了Arisca，一个使用符号计算机代数的开源参数化算术电路验证框架。它建立了一个广义参数空间，统一了以前孤立的技术。为从根本上移植和改进以前的方法，提出了几种算法改进。此外，Arisca将验证范围扩展到包括具有加法和乘法任意组合的一般算术电路。广泛评估表明，Arisca在一系列乘法器基准测试和各种实际算术案例中实现了SOTA性能。
英文摘要：
Formal verification of highly optimized arithmetic circuits at the gate-level remains a significant challenge due to the state space explosion problem. Although Symbolic Computer Algebra (SCA) offers a scalable theoretical foundation by modeling circuits as multivariate polynomials, practical implementations frequently suffer from the explosion of the size of intermediate polynomials. State-of-the-art SCA tools typically rely on fixed heuristics and restrict their application to standard multipliers. A fixed heuristic is insufficient for structurally diverse arithmetic circuits, as it often fails to generalize across all cases. In this paper, we introduce Arisca, an open-source parameterized verification framework for \textbf{Ari}thmetic circuits using \textbf{S}ymbolic \textbf{C}omputer \textbf{A}lgebra. Arisca establishes a generalized parameter space that unifies previously isolated state-of-the-art (SOTA) techniques as specific configurations within a broader algebraic reduction theory. To fundamentally transplant and elevate previous methods, we propose several algorithmic improvements, such as an HA-preserving extraction strategy, density-based vanishing detection, and conservative polynomial size estimation. In addition, Arisca expands the verification scope to encompass general arithmetic circuits with any combination of addition and multiplication, such as multiply-accumulators and dot-product units. Extensive evaluations demonstrate that Arisca achieves SOTA performance in a comprehensive suite of multiplier benchmarks and a diverse array of practical arithmetic cases.
