A Formal Verification Method of Error Correction Code Processors Over Galois-Field Arithmetic
Rei Ueno, Naofumi Homma and Takafumi Aoki
This paper presents a formal approach to verifying Error Correction Code (ECC) processors based on Galois-Field (GF) arithmetic. The proposed method describes GF arithmetic circuits by graph-based representation, called Galois-Field Arithmetic Circuits Graph (GF-ACG), and verifies them by a combination of an algebraic method with a new verification method based on natural deduction for the first-order predicate logic with equal sign. The natural deduction method is suitable for higher-degree GF arithmetic circuits such as in ECC decoders while the conventional methods requires enormous time to verify them or sometimes cannot verify them. In this paper, we apply the proposed method to the design and verifications of various Reed-Solomon (RS) code encoders and decoders. In particular, we confirm that the proposed method can verify RS code decoders with higher-degree functions while the conventional method fails.
Keywords: Formal verification, design methodology for arithmetic circuits, Galois-field, Reed-Solomon code, computer algebra, predicate logic