Download PDFOpen PDF in browser

Rewriting Environment for Arithmetic Circuit Verification

EasyChair Preprint no. 662

9 pagesPublished: December 3, 2018

Abstract

The paper describes a practical, commercial-strength software tool for the verification of integer arithmetic circuits. It covers different types of adders, multipliers, fused add-multiply circuits, and some dividers - the circuits whose computation can be represented as a polynomial. The verification uses an algebraic model of the circuit and is accomplished by rewriting the polynomial of the binary encoding of the primary outputs (output signature), using the polynomial models of the logic gates, into a polynomial over the primary inputs (input signature). The resulting polynomial provides the arithmetic function of the circuit and hence can be used to extract its functional specification from the gate-level implementation. The rewriting uses an efficient \textit{And-Inverter Graph} (AIG) representation to enable extraction of the essential arithmetic components of the circuit. The tool is integrated with the popular ABC system. Its efficiency is illustrated with impressive results for large integer multipliers, fuse-multiply circuits, and divide by constant circuits. The entire verification system is offered in an open source ABC environment together with an extensive set of benchmarks.

Keyphrases: Arithmetic Circuits, computer algebra, formal verification

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:662,
  author = {Cunxi Yu and Atif Yasin and Tiankai Su and Alan Mishchenko and Maciej Ciesielski},
  title = {Rewriting Environment for Arithmetic Circuit Verification},
  howpublished = {EasyChair Preprint no. 662},

  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser