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

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


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 ${\mathbb F}_{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 ${\mathbb F}_{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 ZDD 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 term 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.

Original languageEnglish
Pages (from-to)794-798
Number of pages5
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Issue number3
Publication statusPublished - 2022 Mar 1


  • Formal verification
  • Galois-field (GF) arithmetic circuits
  • Gröbner basis
  • zero-suppressed binary decision diagrams (ZDDs)


Dive into the research topics of 'Efficient Formal Verification of Galois-Field Arithmetic Circuits Using ZDD Representation of Boolean Polynomials'. Together they form a unique fingerprint.

Cite this