Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m)

The Galois field is an important number system that is GF(2m) widely used in applications such as error correction codes (ECC), and complicated combinations of arithmetic operations are performed in those applications. However, few practical formal methods for algorithm verification at the word-level have ever been developed. We have defined a logic system, GF_2m -arithmetic, that can treat non-linear and non-convex GF2m constraints, for describing specifications and implementations of arithmetic algorithms over GF(2m). We have investigated various decision GF_2m -arithmetic and its subclasses, and have performed an automatic correctness proof of a (n, n 4) Reed-Solomon ECC decoding algorithm. Because the correctness criterion is in an efficient subclass of the GF_2m -arithmetic K-field-size independent), the proof is completed in significantly reduced time, less than one second for any and , m ≥ 3 and n ≥ 5, by using a combination of polynomial division and variable elimination over GF(2m), without using any costly techniques such as factoring or a decision over GF(2)that can easily increase the verification time to more than a day.