Equivalence verification of polynomial datapaths with fixed-size bit-vectors using finite ring algebra
Namrata Shekhar, Priyank Kalla, Florian Enescu, S. Gopalakrishnan · 2005
Abstract — This paper addresses the problem of equivalence verification of RTL descriptions. The focus is on datapathoriented 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 m. The verification problem then reduces to that of checking Z2 equivalence of multi-variate polynomials over Z2 m.Thispaper exploits the concepts of polynomial reducibility over Z2m 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