A Formal Verification Method of Error Correction Code Processors Over Galois-Field Arithmetic

作者：Ueno Rei^*; Homma Naofumi; Aoki Takafumi

来源：Journal of Multiple-Valued Logic and Soft Computing, 2016, 26(1-2): 55-73.

• Formal verification
• design methodology for arithmetic circuits
• Galois-field
• Reed-Solomon code
• computer algebra
• predicate logic

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.

• 出版日期2016