TY - GEN
T1 - Formal Verification of Modular Multipliers using Symbolic Computer Algebra and Boolean Satisfiability
AU - Mahzoon, Alireza
AU - Große, Daniel
AU - Scholl, Christoph
AU - Konrad, Alexander
AU - Drechsler, Rolf
PY - 2022/7/10
Y1 - 2022/7/10
N2 - Modular multipliers are the essential components in cryptography and Residue Number System (RNS) designs. Especially, 2n − 1 and 2n + 1 modular multipliers have gained more attention due to their regular structures and a wide variety of applications. However, there is no automated formal verification method to prove the correctness of these multipliers. As a result, bugs might remain undetected after the design phase.
In this paper, we present our modular verifier that combines Symbolic Computer Algebra (SCA) and Boolean Satisfiability (SAT) to prove the correctness of 2n − 1 and 2n + 1 modular multipliers. Our verifier takes advantage of three techniques, i.e. coefficient correction,
SAT-based local vanishing removal, and SAT-based output condition check to overcome the challenges of SCA-based verification. The efficiency of our verifier is demonstrated using an extensive set of modular multipliers with up to several million gates.
AB - Modular multipliers are the essential components in cryptography and Residue Number System (RNS) designs. Especially, 2n − 1 and 2n + 1 modular multipliers have gained more attention due to their regular structures and a wide variety of applications. However, there is no automated formal verification method to prove the correctness of these multipliers. As a result, bugs might remain undetected after the design phase.
In this paper, we present our modular verifier that combines Symbolic Computer Algebra (SCA) and Boolean Satisfiability (SAT) to prove the correctness of 2n − 1 and 2n + 1 modular multipliers. Our verifier takes advantage of three techniques, i.e. coefficient correction,
SAT-based local vanishing removal, and SAT-based output condition check to overcome the challenges of SCA-based verification. The efficiency of our verifier is demonstrated using an extensive set of modular multipliers with up to several million gates.
UR - https://ics.jku.at/files/2022DAC_Formal-Verification-of-Modular-Multipliers-using-SCA-and-SAT.pdf
UR - https://www.scopus.com/pages/publications/85137510565
U2 - 10.1145/3489517.3530605
DO - 10.1145/3489517.3530605
M3 - Conference proceedings
T3 - Proceedings - Design Automation Conference
SP - 1183
EP - 1188
BT - Design Automation Conference 2022
ER -