Formal Verification of Integer Multipliers by Combining Gröbner Basis with Logic Reduction

Amr Sayed Ahmed; Daniel Große; Ulrich Kühne; Mathias Soeken; Rolf Drechsler

In: Design, Automation and Test in Europe (DATE). Design, Automation & Test in Europe (DATE), March 14-18, Dresden, Germany, Pages 1048-1053, 2016.


Formal verification utilizing symbolic computer al-gebra has demonstrated the ability to formally verify largeGalois field arithmetic circuits and basic architectures of integerarithmetic circuits. The technique models the circuit as Gr ̈obnerbasis polynomials and reduces the polynomial equation of thecircuit specification wrt. the polynomials model. However, duringthe Gr ̈obner basis reduction, the technique suffers from expo-nential blow-up in the size of the polynomials, if it is appliedon parallel adders and recoded multipliers. In this paper, weaddress the reasons of this blow-up and present an approachthat allows to apply the technique on basic and complex parallelarchitectures of multipliers. The approach is based on applyinga logic reduction rule during Gr ̈obner basis rewriting. The ruleuses structural circuit information to remove terms that evaluateto zero before their blow-up. The experiments show that theapproach is applicable up to 128 bit multipliers

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence