Efficient Grobner Basis Reductions for Formal Verification of Galois Field Arithmetic Circuits

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 F-2k 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 Grobner 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 Grobner bases over F-2k, we show that this term order renders the set of polynomials itself a minimal Grobner basis of this ideal. Consequently, the verification test reduces to a much simpler case of Grobner basis reduction via polynomial division, significantly enhancing verification efficiency. To further improve our approach, we exploit the concepts presented in the F4 algorithm for Grobner 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 F-2163-whereas verification utilizing contemporary techniques proves infeasible.