Verification of arithmetic datapaths using polynomial function models and congruence solving

Abstract— 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 : Z2n1 × Z2n2 × · · · × Z2nd → Z2m . This enables the use of modulo-arithmetic based decision procedures for solving such problems in one unified domain. We devise a decision procedure using Newton’s 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...

• Type: Conference
• Year: 2008
• Where: ICCAD
• Authors: Neal Tew, Priyank Kalla, Namrata Shekhar, Sivaram Gopalakrishnan
• Keywords: Arithmetic Datapath Designs, Arithmetic Datapaths, Arithmetic Operations, Hardware, ICCAD 2008