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

研究成果: Conference contribution

2 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトルProceedings - 2020 IEEE 50th International Symposium on Multiple-Valued Logic, ISMVL 2020
出版社IEEE Computer Society
ページ46-51
ページ数6
ISBN(電子版)9781728154060
DOI
出版ステータスPublished - 2020 11
イベント50th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2020 - Miyazaki, Japan
継続期間: 2020 11 92020 11 11

出版物シリーズ

名前Proceedings of The International Symposium on Multiple-Valued Logic
2020-November
ISSN(印刷版)0195-623X

Conference

Conference50th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2020
国/地域Japan
CityMiyazaki
Period20/11/920/11/11

ASJC Scopus subject areas

  • コンピュータ サイエンス(全般)
  • 数学 (全般)

フィンガープリント

「Effective Formal Verification for Galois-field Arithmetic Circuits with Multiple-Valued Characteristics」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル