Equivalence verification of arithmetic datapaths with multiple word-length operands

This paper addresses the problem of equivalence verification of RTL descriptions that implement arithmetic computations (add, mult, shift) over bit-vectors 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 2ⁿ - 1; i.e. integers reduced modulo 2ⁿ. Therefore, to verify bit-vector arithmetic over multiple word-length operands, we model the RTL datapath as a polynomial function from Z_2n1 times Z_2n2 times ... Z_2nd to Z_2m. Subsequently, RTL equivalence f equiv g is solved by proving whether (f - g) equiv 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 arithmetic datapaths at RTL where contemporary approaches prove to be in feasible