Arisca: A Parameterized Symbolic Algebra Framework for Arithmetic Circuit Verification
2026-07-11 • Symbolic Computation
Symbolic Computation
AI summaryⓘ
The authors address the difficulty of verifying complex arithmetic circuits, which can become too large to analyze with current methods. They created Arisca, an open-source tool that uses symbolic computer algebra but improves on prior techniques by allowing more flexible and general settings. Arisca introduces new algorithms to better handle different circuit structures and can verify a wider variety of arithmetic circuits, like those combining addition and multiplication. Their tests show that Arisca performs as well or better than existing tools on standard and more complex circuit designs.
Formal VerificationArithmetic CircuitsGate-levelState Space ExplosionSymbolic Computer AlgebraPolynomial ReductionMultiply-AccumulatorsDot-Product UnitsHeuristics
Authors
Kezhi Li, Min Li, Qiang Xu
Abstract
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.