Galois field arithmetic is a critical component in communication and security-related hardware, requiring dedicated arithmetic architectures for better performance. In many Galois field applications, such as cryptography, the data-path size in the circuits can be very large. Formal verification of such circuits is beyond the capabilities of contemporary verification techniques. This paper addresses formal verification of combinational arithmetic circuits over Galois fields of the type${\BBF}_{2^{k}}$using a computer-algebra/algebraic-geometry-based approach. The verification problem is formulated as membership testing of a given specification polynomial in a corresponding ideal generated by the circuit constraints. Ideal membership testing requires the computation of a Gröbner basis, which is computationally very expensive. To overcome this limitation, we analyze the circuit topology and derive a term order to represent the polynomials. Subsequently, using the theory of Gröbner bases over${\BBF}_{2^{k}}$, we show that this term order renders the set of polynomials itself a minimal Gröbner basis of this ideal. Consequently, the verification test reduces to a much simpler case of Gröbner basis reduction via polynomial division, significantly enhancing verification efficiency. To further improve our approach, we exploit the concepts presented in the$F4$algorithm for Gröbner basis, and show that the verification test can be formulated as Gaussian elimination on a matrix representation of the problem. Finally, we demonstrate the ability of our approach to verify the correctness of, and detect bugs in, up to 163-bit circuits in${\BBF}_{2^{163}}$—whereas verification utilizing contemporary techniques proves infeasible.

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)[x1, x2, ... , xd] and the verification problem is formulated as a membership test in a corresponding (radical) ideal. This requires the computation of a Gröbner 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 Gröbner bases over Galois fields, we prove that this term order renders the set of polynomials itself a Gröbner 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(2163); whereas contemporary approaches are infeasible.