Sciweavers

29
Voted
ICCAD
2005
IEEE

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

14 years 7 months ago
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.
Namrata Shekhar, Priyank Kalla, Florian Enescu, Si
Added 16 Mar 2010
Updated 16 Mar 2010
Type Conference
Year 2005
Where ICCAD
Authors Namrata Shekhar, Priyank Kalla, Florian Enescu, Sivaram Gopalakrishnan
Comments (0)