Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability

Alireza Mahzoon, Daniel Große, Christoph Scholl, Alexander Konrad, Rolf Drechsler

2022Proceedings of the 59th ACM/IEEE Design Automation Conference15 citationsDOI

Abstract

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.

Topics & Concepts

CorrectnessComputer scienceModular designResidue number systemModular arithmeticFormal verificationTheoretical computer scienceProgramming languageCryptographyFormal equivalence checkingSatisfiabilityBoolean satisfiability problemSymbolic computationArithmeticAlgorithmMathematicsMathematical analysisCryptography and Residue ArithmeticCryptographic Implementations and SecuritySecurity and Verification in Computing