Efficient Formal Verification of Galois-Field Arithmetic Circuits Using ZDD Representation of Boolean Polynomials

研究成果: Article査読

抄録

In this study, we present a new formal method for verifying the functionality of Galois-field (GF) arithmetic circuits. Assuming that the input–output relation (i.e., the specification of a GF arithmetic circuit) can be represented as polynomials over 2, the proposed method formally checks the equivalence between GF polynomials derived from a netlist and the specification. To efficiently verify the equivalence, we employ a zero-suppressed binary decision diagram (ZDD) to represent polynomials over 2. Even though polynomial reduction is the most time-consuming process of verification (i.e., equivalence checking), our new algorithm can efficiently reduce the GF polynomials in the form of a zero-suppressed binary decision diagram derived from the target netlist. The proposed algorithm derives the polynomials representing all intermediate nodes (i.e., the outputs of all gates) in the order from primary inputs to those primary outputs that are in accordance with the reverse topological traversal order. We demonstrated the efficiency and effectiveness of the proposed method via a set of experimental verifications. In particular, we confirmed that the proposed method can verify practical GF multipliers (including those used in standardized elliptic curve cryptography) approximately 30 times faster on average and at most 170 times faster than the best conventional method.

本文言語English
ジャーナルIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
DOI
出版ステータスAccepted/In press - 2021

ASJC Scopus subject areas

  • ソフトウェア
  • コンピュータ グラフィックスおよびコンピュータ支援設計
  • 電子工学および電気工学

フィンガープリント

「Efficient Formal Verification of Galois-Field Arithmetic Circuits Using ZDD Representation of Boolean Polynomials」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル