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(2m). The verification problem then reduces to that of checking equivalence of over Z(2m): in other words, to prove f(x)%2(m) equivalent to g(x)%2(m). This paper transforms the equivalence verification problem into proving (f(x)-g(x))%2(m) equivalent to 0. Exploiting the theory of vanishing polynomials overfinite integer rings, a systematic algorithmic procedure is derived to establish whether or not a given polynomial vanishes (always evaluates to 0) over Z2(m). Experiments demonstrate the effectiveness of our approach over contemporary techniques.