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/sub 2//sup m/. The verification problem then reduces to that of checking equivalence of multi-variate polynomials over Z/sub 2//sup m/. This paper exploits the concepts of polynomial reducibility over Z/sub 2//sup m/ and derives an algorithmic procedure to transform a given polynomial into a unique canonical form modulo 2/sup m/. Equivalence testing is then carried out by coefficient matching. Experiments demonstrate the effectiveness of our approach over contemporary techniques.