Formal Approach for Verifying Galois Field Arithmetic Circuits of Higher Degrees

Rei Ueno, Naofumi Homma, Yukihiro Sugawara, Takafumi Aoki

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)

Abstract

This paper presents an efficient approach to verifying higher-degree Galois-field (GF) arithmetic circuits. The proposed method describes GF arithmetic circuits using a mathematical graph-based representation and verifies them by a combination of algebraic transformations and a new verification method based on natural deduction for first-order predicate logic with equal sign. The natural deduction method can verify one type of higher-degree GF arithmetic circuit efficiently while the existing methods require an enormous amount of time, if they can verify them at all. In this paper, we first apply the proposed method to the design and verification of various Reed-Solomon (RS) code decoders. We confirm that the proposed method can verify RS decoders with higher-degree functions while the existing method needs a lot of time or fail. In particular, we show that the proposed method can be applied to practical decoders with 8-bit symbols, which are performed with up to 2,040-bit operands. We then demonstrate the design and verification of the Advanced Encryption Standard (AES) encryption and decryption processors. As a result, the proposed method successfully verifies the AES decryption datapath while an existing method fails.

Original languageEnglish
Article number7555392
Pages (from-to)431-442
Number of pages12
JournalIEEE Transactions on Computers
Volume66
Issue number3
DOIs
Publication statusPublished - 2017 Mar 1

Keywords

  • Formal verification
  • Galois field
  • advanced encryption standard
  • arithmetic logic
  • computer algebra
  • design methodology for arithmetic circuits

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'Formal Approach for Verifying Galois Field Arithmetic Circuits of Higher Degrees'. Together they form a unique fingerprint.

Cite this