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