# Spectral Approach to Verifying Non-linear Arithmetic Circuits

## TL;DR

This paper introduces a novel spectral algebraic method for verifying non-linear integer arithmetic circuits efficiently, leveraging algebraic spectra and local polynomial rewriting to improve speed and accuracy.

## Contribution

It proposes a new algebraic spectral model and a coefficient propagation technique for faster verification of complex non-linear arithmetic circuits.

## Key findings

- Successfully verified circuits up to 1024 bits with over 12 million gates
- Achieved significant speedup over previous verification methods
- Demonstrated effectiveness on standard and Booth multipliers

## Abstract

This paper presents a fast and effective computer algebraic method for analyzing and verifying non-linear integer arithmetic circuits using a novel algebraic spectral model. It introduces a concept of algebraic spectrum, a numerical form of polynomial expression; it uses the distribution of coefficients of the monomials to determine the type of arithmetic function under verification. In contrast to previous works, the proof of functional correctness is achieved by computing an algebraic spectrum combined with a local rewriting of word-level polynomials. The speedup is achieved by propagating coefficients through the circuit using And-Inverter Graph (AIG) datastructure. The effectiveness of the method is demonstrated with experiments including standard and Booth multipliers, and other synthesized non-linear arithmetic circuits up to 1024 bits containing over 12 million gates.