Arisca: A Parameterized Symbolic Algebra Framework for Arithmetic Circuit Verification

From bibtex.

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 Arithmetic circuits using Symbolic Computer Algebra. Arisca establishes a generalized parameter space that unifies previously isolated state-of-the-art 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.