An Efficient Approach to Verifying Galois-Field Arithmetic Circuits of Higher Degrees and Its Application to ECC Decoders

This paper presents an efficient approach to verifying higher-degree Galois-Field(GF) arithmetic circuits. The proposed method describes GF arithmetic circuits by graph-based representation, and verifies them by a combination of algebraic method with a new verification method based on natural deduction for the first-order predicate logic with equal sign. The natural deduction method can verify kind of higher-degree GF arithmetic circuits efficiently 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 decoders. We confirm that the proposed method can verify RS code decoders with higher-degree functions while the conventional method fails. In particular, we show that the proposed method can be applied to practical decoders with 8-bit symbols.