Verification of arithmetic datapaths using polynomial function models and congruence solving

This paper addresses the problem of solving finite word-length (bit-vector) arithmetic with applications to equivalence verification of arithmetic datapaths. Arithmetic datapath designs perform a sequence of add, mult, shift, compare, concatenate, extract, etc., operations over bit-vectors. We show that such arithmetic operations can be modeled, as constraints, using a system of polynomial functions of the type f : Z₂n₁ times Z₂n₂ times ldrldrldr times Z₂n_d rarr Z₂m. This enables the use of modulo-arithmetic based decision procedures for solving such problems in one unified domain. We devise a decision procedure using Newtonpsilas p-adic iteration to solve such arithmetic with composite moduli, while properly accounting for the word-sizes of the operands. We describe our implementation and show how the basic p-adic approach can be improved upon. Experiments are performed over some communication and signal processing designs that perform non-linear and polynomial arithmetic over word-level inputs. Results demonstrate the potential and limitations of our approach, when compared against SAT-based approaches.