  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.
