TY - JOUR

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

AU - Ito, Akira

AU - Ueno, Rei

AU - Homma, Naofumi

N1 - Funding Information:
This work was supported in part by Japan Society For The Promotion Of Science (JSPS) KAKENHI under Grant 17H00729; in part by the JSPS Research Fellow under Grant H20J128870; and in part by the Secom Science and Technology Foundation.
Publisher Copyright:
© 1982-2012 IEEE.

PY - 2022/3/1

Y1 - 2022/3/1

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

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

KW - Formal verification

KW - Galois-field (GF) arithmetic circuits

KW - GrÃ¶bner basis

KW - zero-suppressed binary decision diagrams (ZDDs)

UR - http://www.scopus.com/inward/record.url?scp=85100920675&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85100920675&partnerID=8YFLogxK

U2 - 10.1109/TCAD.2021.3059924

DO - 10.1109/TCAD.2021.3059924

M3 - Article

AN - SCOPUS:85100920675

SN - 0278-0070

VL - 41

SP - 794

EP - 798

JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

IS - 3

ER -