Sciweavers

DATE
2006
IEEE

Equivalence verification of arithmetic datapaths with multiple word-length operands

14 years 3 months ago
Equivalence verification of arithmetic datapaths with multiple word-length operands
Abstract: This paper addresses the problem of equivalence verification of RTL descriptions that implement arithmetic computations (add, mult, shift) over bitvectors that have differing bit-widths. Such designs are found in many DSP applications where the widths of input and output bit-vectors are dictated by the desired precision. A bit-vector of size n can represent integer values from 0 to 2n − 1; i.e. integers reduced modulo 2n . Therefore, to verify bit-vector arithmetic over multiple wordlength operands, we model the RTL datapath as a polynomial function from Z2n1 × Z2n2 × · · · × Z2nd to Z2m . Subsequently, RTL equivalence f ≡ g is solved by proving whether (f − g) ≡ 0 over such mappings. Exploiting concepts from number theory and commutative algebra, a systematic, complete algorithmic procedure is derived for this purpose. Experimentally, we demonstrate how this approach can be applied within a practical CAD setting. Using our approach, we verify a set of arithme...
Namrata Shekhar, Priyank Kalla, Florian Enescu
Added 10 Jun 2010
Updated 10 Jun 2010
Type Conference
Year 2006
Where DATE
Authors Namrata Shekhar, Priyank Kalla, Florian Enescu
Comments (0)