Authors: Daniel Große, Universität Bremen, DE; Rolf Drechsler, Universität Bremen, DE; Amr Sayed Ahmed, Universität Bremen, DE; Mathias Soeken, Universität Bremen, DE; Ulrich Kühne, Universität Bremen, DE
Best paper candidate
Abstract:
Formal verification utilizing symbolic computer algebra has demonstrated the ability to formally verify large Galois field arithmetic circuits and basic architectures of integer arithmetic circuits. The technique models the circuit as Gröbner basis polynomials and reduces the polynomial equation of the circuit specification wrt. the polynomials model. However, during the Gröbner basis reduction, the technique suffers from exponential blow-up in the size of the polynomials, if it is applied on parallel adders and recoded multipliers. In this paper, we address the reasons of this blow-up and present an approach that allows to apply the technique on basic and complex parallel architectures of multipliers. The approach is based on applying a logic reduction rule during Gröbner basis rewriting. The rule uses structural circuit information to remove terms that evaluate to zero before their blow-up. The experiments show that the approach is applicable up to 128 bit multiplier.
Publication Date: 2016/03/14
Location of Publication: In Design, Automation and Test in Europe (DATE), Dresden, DE, 2016
Keyword: Verification
