Effective Formal Verification for Galois-field Arithmetic Circuits with Multiple-Valued Characteristics

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

This study presents a new formal verification method for Galois-field (GF) arithmetic circuits with the characteristics of more-than two. The proposed method formally verifies the correctness of circuit functionality (i.e., the inputoutput relations given as GF-polynomials) by checking the equivalence between a specification and a gate-level netlist. In the proposed method, we represent a netlist as simultaneous algebraic equations and solve them based on a new polynomial reduction method efficiently applicable to arithmetic over extension fields {{\mathbb{F}}_{{p^m}}}, where the characteristic p is larger than two. Using reverse topological term order to derive the Gröbner basis, our method can complete the verification even when a target circuit includes bugs. Our experimental results show that the proposed method can efficiently verify practical {{\mathbb{F}}_{{p^m}}} arithmetic circuits, including those used in modern cryptography.

Original languageEnglish
Title of host publicationProceedings - 2020 IEEE 50th International Symposium on Multiple-Valued Logic, ISMVL 2020
PublisherIEEE Computer Society
Pages46-51
Number of pages6
ISBN (Electronic)9781728154060
DOIs
Publication statusPublished - 2020 Nov
Event50th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2020 - Miyazaki, Japan
Duration: 2020 Nov 92020 Nov 11

Publication series

NameProceedings of The International Symposium on Multiple-Valued Logic
Volume2020-November
ISSN (Print)0195-623X

Conference

Conference50th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2020
Country/TerritoryJapan
CityMiyazaki
Period20/11/920/11/11

Keywords

  • Formal verification
  • Galois-field arithmetic circuits
  • Multiple-valued logic

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)

Fingerprint

Dive into the research topics of 'Effective Formal Verification for Galois-field Arithmetic Circuits with Multiple-Valued Characteristics'. Together they form a unique fingerprint.

Cite this