Exploiting vanishing polynomials for equivalence verification of fixed-size arithmetic datapaths

This paper addresses the problem of equivalence verification of high-level/RTL descriptions. The focus is on datapath-oriented designs that implement univariate polynomial computations over fixed-size bit-vectors. When the size (m) of the entire datapath is kept constant, fixed-size bit-vector arithmetic manifests itself as polynomial algebra over finite integer rings of residue classes Z₂^m. The verification problem then reduces to that of checking equivalence of over Z₂^m in other words, to prove f(x)%2^m ≡ g(x)%2^m. This paper transforms the equivalence verification problem into proving (f(x) - g(x))%2^m ≡ 0. Exploiting the theory of vanishing polynomials over finite integer rings, a systematic algorithmic procedure is derived to establish whether or not a given polynomial vanishes (always evaluates to 0) over Z₂^m. Experiments demonstrate the effectiveness of our approach over contemporary techniques.