Efficient Gröbner basis reductions for formal verification of galois field multipliers
Jinpeng Lv, Priyank Kalla, Florian Enescu · Design, Automation, and Test in Europe · 2012
Galois field arithmetic finds application in many areas, such as cryptography, error correction codes, signal processing, etc. Multiplication lies at the core of most Galois field computations. This paper addresses the problem of formal verification of hardware implementations of (modulo) multipliers over Galois fields of the type F 2k , using a computer-algebra/algebraic-geometry based approach. The multiplier circuit is modeled as a polynomial system in F 2k [x 1 , x 2 , … , x d ] and the verification problem is formulated as a membership test in a corresponding (radical) ideal. This requires the computation of a Grobner basis, which can be computationally intensive. To overcome this limitation, we analyze the circuit topology and derive a term order to represent the polynomials. Subsequently, using the theory of Grobner bases over Galois fields, we prove that this term order renders the set of polynomials itself a Grobner basis of this ideal - thus significantly improving verification. Using our approach, we can verify the correctness of, and detect bugs in, upto 163-bit circuits in F 2 163 ; whereas contemporary approaches are infeasible.