The search functionality is under construction.
The search functionality is under construction.

An Algebraic Approach to Verifying Galois-Field Arithmetic Circuits with Multiple-Valued Characteristics

Akira ITO, Rei UENO, Naofumi HOMMA

  • Full Text Views

    0

  • Cite this

Summary :

This study presents a formal verification method for Galois-field (GF) arithmetic circuits with the characteristics of more than two values. The proposed method formally verifies the correctness of circuit functionality (i.e., the input-output relations given as GF-polynomials) by checking the equivalence between a specification and a gate-level netlist. We represent a netlist using simultaneous algebraic equations and solve them based on a novel polynomial reduction method that can be efficiently applied to arithmetic over extension fields $mathbb{F}_{p^m}$, where the characteristic p is larger than two. By using the reverse topological term order to derive the Gröbner basis, our method can complete the verification, even when a target circuit includes bugs. In addition, we introduce an extension of the Galois-Field binary moment diagrams to perform the polynomial reductions faster. Our experimental results show that the proposed method can efficiently verify practical $mathbb{F}_{p^m}$ arithmetic circuits, including those used in modern cryptography. Moreover, we demonstrate that the extended polynomial reduction technique can enable verification that is up to approximately five times faster than the original one.

Publication
IEICE TRANSACTIONS on Information Vol.E104-D No.8 pp.1083-1091
Publication Date
2021/08/01
Publicized
2021/04/28
Online ISSN
1745-1361
DOI
10.1587/transinf.2020LOP0004
Type of Manuscript
Special Section PAPER (Special Section on Multiple-Valued Logic and VLSI Computing)
Category
Logic Design

Authors

Akira ITO
  Tohoku University
Rei UENO
  Tohoku University
Naofumi HOMMA
  Tohoku University

Keyword