A formal verification method of error correction code processors over Galois-field arithmetic

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish
Pages (from-to)55-73
Number of pages19
JournalJournal of Multiple-Valued Logic and Soft Computing
Volume26
Issue number1-2
Publication statusPublished - 2016

Keywords

  • Computer algebra
  • Design methodology for arithmetic circuits
  • Formal verification
  • Galois-field
  • Predicate logic
  • Reed-Solomon code

ASJC Scopus subject areas

  • Software
  • Logic
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'A formal verification method of error correction code processors over Galois-field arithmetic'. Together they form a unique fingerprint.

  • Cite this