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

• Type: Conference
• Year: 2005
• Where: ICCAD
• Authors: Namrata Shekhar, Priyank Kalla, Florian Enescu, Sivaram Gopalakrishnan
• Keywords: Hardware, ICCAD 2005, Polynomial Algebra, Polynomial Computations, Polynomial Reducibility