Title :
An Efficient Approach to Verifying Galois-Field Arithmetic Circuits of Higher Degrees and Its Application to ECC Decoders
Author :
Ueno, Risako ; Okamoto, K. ; Hommam, Naofumi ; Aoki, Toyohiro
Author_Institution :
Grad. Sch. of Inf. Sci., Tohoku Univ., Sendai, Japan
Abstract :
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.
Keywords :
Galois fields; Reed-Solomon codes; arithmetic codes; decoding; error correction codes; formal logic; formal verification; graph theory; ECC decoders; Galois-field arithmetic circuit verification method; RS code decoders; Reed-Solomon code decoders; algebraic method; error correction code; first-order predicate logic; formal verification; graph-based representation; higher-degree GF arithmetic circuit; natural deduction method; Decoding; Estimation; Mathematical model; Polynomials; Reactive power; Reed-Solomon codes; Galois fi eld; Reed-Solomon code; arithmetic circuits; computer algebra; formal verification; predicate logic;
Conference_Titel :
Multiple-Valued Logic (ISMVL), 2014 IEEE 44th International Symposium on
Conference_Location :
Bremen
DOI :
10.1109/ISMVL.2014.33