Towards efficient verification of arithmetic algorithms over galois fields GF(2m)

Abstract

The Galois field GF(2m) is an important number system that is 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, (formula presented) -arithmetic, that can treat non-linear and non-convex constraints, for describing specifications and implementations of arithmetic algorithms over GF(2m). We have investigated various decision techniques for the (formula presented) -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 (formula presented) -arithmetic (k -field-size independent), the proof is completed in significantly reduced time, less than one second for any 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.