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...

• Type: Conference
• Year: 2006
• Where: DATE
• Authors: Namrata Shekhar, Priyank Kalla, Florian Enescu
• Keywords: DATE 2006, Hardware, RTL Datapath, RTL Descriptions, RTL Equivalence