Equivalence verification of polynomial datapaths with fixed-size bit-vectors using finite ring algebra

This paper addresses the problem of equivalence verification of RTL descriptions. The focus is on datapath-oriented designs that implement 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 multi-variate polynomials over Z₂^m. This paper exploits the concepts of polynomial reducibility over Z₂^m and derives an algorithmic procedure to transform a given polynomial into a unique canonical form modulo 2^m. Equivalence testing is then carried out by coefficient matching. Experiments demonstrate the effectiveness of our approach over contemporary techniques.