Recurrence relations revisited: Scalable verification of bit level multiplier circuits

Although a lot of effort has been spent on verifying arithmetic designs, it is still a problem that has no general robust automated solution. One major challenge is verifying large scale multiplier circuits. For this purpose, we revisit the idea of using functional properties of the multiplication function, which can be expressed by recurrence equations. Then, instead of proving the equivalence of the implementation and a specification, the verification task is to show that the implementation satisfies the recurrence equation. We propose an approach which makes this verification task practically feasible for large scale multiplier circuits. Based on a combined add/multiply recurrence equation we can make efficient use of case splitting wrt. The partial products of the multiplier. As a result, the problem is split such that only a small part of the multiplier will be checked in every case, thereby avoiding redundant checks between the cases. Overall, our approach allows to verify a variety of multiplier designs in practical time. We present results for multipliers up to 128 bits.