Simulation bounds for equivalence verification of arithmetic datapaths with finite word-length operands

This paper addresses simulation-based verification of high-level descriptions of arithmetic datapaths. Instances of such designs are commonly found in DSP for audio, video and multimedia applications, where the word-lengths of input/output bit-vectors are fixed according to the desired precision. Initial descriptions of such systems are usually specified as Matlab/C code. These are then automatically translated into behavioural/RTL descriptions (HDL) for subsequent hardware synthesis. In order to verify that the initial Matlab/C model is bit-true equivalent to the translated RTL, how many simulation vectors need to be applied? This paper explores results from number theory and commutative algebra to show that exhaustive simulation is not necessary for testing their equivalence. In particular, we derive an upper bound on the number of simulation vectors required to prove equivalence or identify bugs. These vectors cannot be arbitrarily generated; we determine exactly those vectors that need to be simulated. Extensive experiments are performed within practical CAD settings to demonstrate the validity and applicability of these results.