Verification of arithmetic datapaths using polynomial function models and congruence solving
Neal Tew, Priyank Kalla, Namrata Shekhar, Sivaram Gopalakrishnan · 2008
Abstract — This paper addresses the problem of solving fi-nite word-length (bit-vector) arithmetic with applications to equivalence verification of arithmetic datapaths. Arithmetic datapath designs perform a sequence of add, mult, shift, com-pare, 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: Z2n1 × Z2n2 × · · · × Z2nd → Z2m. This enables the use of modulo-arithmetic based decision procedures for solv-ing such problems in one unified domain. We devise a decision procedure using Newton’s p-adic iteration to solve such arith-metic with composite moduli, while properly accounting for the word-sizes of the operands. We describe our implemen-tation and show how the basic p-adic approach can be im-proved upon. Experiments are performed over some commu-nication 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. I.