Effective Formal Verification for Galois-field Arithmetic Circuits with Multiple-Valued Characteristics

This study presents a new formal verification method for Galois-field (GF) arithmetic circuits with the characteristics of more-than two. The proposed method formally verifies the correctness of circuit functionality (i.e., the inputoutput relations given as GF-polynomials) by checking the equivalence between a specification and a gate-level netlist. In the proposed method, we represent a netlist as simultaneous algebraic equations and solve them based on a new polynomial reduction method efficiently applicable to arithmetic over extension fields {{\mathbb{F}}_{{p^m}}}, where the characteristic p is larger than two. Using reverse topological term order to derive the Gröbner basis, our method can complete the verification even when a target circuit includes bugs. Our experimental results show that the proposed method can efficiently verify practical {{\mathbb{F}}_{{p^m}}} arithmetic circuits, including those used in modern cryptography.