Formal Verification Of Integer Multipliers By Combining Grobner 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 Grobner basis polynomials and reduces the polynomial equation of the circuit specification wrt. the polynomials model. However, during the Grobner 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 Grobner 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.