Formal Verification of Modular Multipliers using Symbolic Computer Algebra and Boolean Satisfiability
TimeThursday, July 14th4:10pm - 4:30pm PDT
Location3000, Level 3
Event Type
Research Manuscript
Design Verification and Validation
DescriptionModular multipliers are the essential components in cryptography and Residue Number System designs.
Especially, 2^n-1 and 2^n+1 modular multipliers have gained more attention due to their regular structure and a wide variety of applications.

In this paper, we present our modular verifier that combines Symbolic Computer Algebra and Boolean Satisfiability to prove the correctness of modular multipliers.
Our verifier uses 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 millions of gates.