基于形式化方法的有限域乘法器的建模与验证

摘要：

针对有限域乘法器设计正确性的问题进行研究,阐述了有限域乘法器在高阶逻辑定理证明器HOL4中进行形式化建模和验证的过程.通过分析电路的结构特性和时序特性,提出了结合层次化和基于周期的形式化建模方法,构建4位多项式基有限域乘法器的形式化模型;最后在HOL4系统中完成对其相关性质的验证.实验结果证明了该有限域乘法器设计的正确性,同时表明所提出的建模方法对时序逻辑电路的验证是有效的.

关键词：形式化方法、定理证明、有限域乘法器、时序逻辑电路、HOL4

所属期刊栏目：44

分类号：TP332(计算技术、计算机技术)

资助基金：国家自然科学基金61572331

在线出版日期：2018-01-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：109-113