The search functionality is under construction.

The search functionality is under construction.

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

Akira ITO

Tohoku University

Rei UENO

Tohoku University

Naofumi HOMMA

Tohoku University

The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.

Copy

Akira ITO, Rei UENO, Naofumi HOMMA, "An Algebraic Approach to Verifying Galois-Field Arithmetic Circuits with Multiple-Valued Characteristics" in IEICE TRANSACTIONS on Information,
vol. E104-D, no. 8, pp. 1083-1091, August 2021, doi: 10.1587/transinf.2020LOP0004.

Abstract: 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.

URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2020LOP0004/_p

Copy

@ARTICLE{e104-d_8_1083,

author={Akira ITO, Rei UENO, Naofumi HOMMA, },

journal={IEICE TRANSACTIONS on Information},

title={An Algebraic Approach to Verifying Galois-Field Arithmetic Circuits with Multiple-Valued Characteristics},

year={2021},

volume={E104-D},

number={8},

pages={1083-1091},

abstract={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.},

keywords={},

doi={10.1587/transinf.2020LOP0004},

ISSN={1745-1361},

month={August},}

Copy

TY - JOUR

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

T2 - IEICE TRANSACTIONS on Information

SP - 1083

EP - 1091

AU - Akira ITO

AU - Rei UENO

AU - Naofumi HOMMA

PY - 2021

DO - 10.1587/transinf.2020LOP0004

JO - IEICE TRANSACTIONS on Information

SN - 1745-1361

VL - E104-D

IS - 8

JA - IEICE TRANSACTIONS on Information

Y1 - August 2021

AB - 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.

ER -