Formal Verification of Galois Field Multipliers Using Computer Algebra Techniques

Finite (Galois) field arithmetic finds applications in cryptography, error correction codes, signal processing, etc. Multiplication usually lies at the core of all Galois field computations and is a high-complexity operation. This paper addresses the problem of formal verification of hardware implementations of modulo-multipliers over Galois fields of the type F₂k, using a computer-algebra/algebraic-geometry based approach. The multiplier circuit is modeled as a polynomial system in F₂k[x₁,x₂,⋯,x_d] and the verification test is formulated as a Nullstellensatz proof over the finite field. A Grobner basis engine is used as the underlying computational framework. The efficiency of Grobner basis computations depends heavily upon the variable (and term) ordering used to represent and manipulate the polynomials. We present a variable (and term) ordering heuristic that significantly improves the efficiency of Grobner basis engines. Using our approach, we can verify the correctness of up to 96-bit multipliers, whereas contemporary BDDs/SAT/SMT-solver based methods are infeasible.