Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

ICCAD

2008

IEEE

2008

IEEE

Abstract— This paper addresses the problem of solving ﬁnite word-length (bit-vector) arithmetic with applications to equivalence veriﬁcation 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 uniﬁed 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...

Related Content

Added |
16 Mar 2010 |

Updated |
16 Mar 2010 |

Type |
Conference |

Year |
2008 |

Where |
ICCAD |

Authors |
Neal Tew, Priyank Kalla, Namrata Shekhar, Sivaram Gopalakrishnan |

Comments (0)