Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability
Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability
复制标题
使用符号计算机代数和布尔可满足性对模乘法器进行形式化验证
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
R. Drechsler
中科院分区：
文献类型：
--
作者：
Alireza Mahzoon;Daniel Große;Christoph Scholl;Alexander Konrad;R. Drechsler
模块化乘数是密码学和残基编号系统（RNS）设计中的重要组成部分。特别是，由于其规则结构和多种应用，2N -1和2N + 1模块化乘数引起了更多的关注。但是，没有自动化的正式验证方法来证明这些乘数的正确性。结果，在设计阶段之后可能仍未发现错误。在本文中，我们介绍了结合符号计算机代数（SCA）和布尔值满意度（SAT）的模块化验证器，以证明2n -1和2n + 1模块化乘数的正确性。我们的验证者利用三种技术，即系数校正，基于SAT的本地消失以及基于SAT的输出条件检查，以克服基于SCA的验证的挑战。使用一组大量的模块化乘数（多达几百万个大门）证明了我们验证者的效率。
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.