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

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 multipliers.


Published in:
Proceedings of the Design, Automation and Test in Europe Conference (DATE)
Presented at:
Design, Automation and Test in Europe (DATE), Dresden, Germany, March 14-18, 2016
Year:
2016
Publisher:
New York, IEEE
ISBN:
978-3-9815-3707-9
Laboratories:




 Record created 2016-02-16, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)