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 datapathoriented designs that implement univariate polynomial computations over fixed-size bit-vectors. Such designs, found in many DSP applications, perform a sequence of ADD, MULT, SHIFT type of algebraic computations that can be modeled as univariate polynomials of finite degree. Often, the datapath size (m) of the entire design is kept constant- fixed according to the size of the bit-vector operands. Such fixed-size bitvector arithmetic manifests itself as polynomial algebra over finite integer rings of residue classes Z2m. RTL verification problem then reduces to that of checking polynomial equivalence in Z2m: in other words, to prove f(x)%2m ≡ g(x)%2m. This paper formulates the equivalence verification problem f(x)%2m ≡ g(x)%2m by transforming it into proving (f(x) − g(x))%2m ≡ 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 Z2m. The algorithm has been implemented in MAPLE. Using our approach, symbolically distinct but computationally equivalent RTL descriptions of various multi-media and elementary function computations have been correctly verified; where BDD, BMD, SAT and MILP-based methods are found to be impractical. I