期刊文献+

基于形式化方法的有限域乘法器的建模与验证 被引量:4

Modeling and verification of finite field multiplier using formal method
下载PDF
导出
摘要 针对有限域乘法器设计正确性的问题进行研究,阐述了有限域乘法器在高阶逻辑定理证明器HOL4中进行形式化建模和验证的过程。通过分析电路的结构特性和时序特性,提出了结合层次化和基于周期的形式化建模方法,构建4位多项式基有限域乘法器的形式化模型;最后在HOL4系统中完成对其相关性质的验证。实验结果证明了该有限域乘法器设计的正确性,同时表明所提出的建模方法对时序逻辑电路的验证是有效的。 This paper focused on the correctness of finite field multiplier, and described the detailed process of formal modeling and verification of finite field multiplier in higher-order logic theorem prover HOL4. Based on analyzing the structural characteris-tics and time sequence characteristics of the circuit, a formal modeling method which combine hierarchical technology and periodic-based method is proposed. And the formal model of a 4-bit polynomial-based finite field multiplier has been constructed. Finally,its properties are proved in the HOL4 system. The experimental results show the correctness of the finite field multiplier design,and show that the proposed modeling method is valid for the verification of sequence circuit.
出处 《电子技术应用》 2018年第1期109-113,共5页 Application of Electronic Technique
基金 国家自然科学基金(61572331)
关键词 形式化方法 定理证明 有限域乘法器 时序逻辑电路 HOL4 formal method theorem proving finite field multiplier sequence circuit HOL4
  • 相关文献

同被引文献33

引证文献4

二级引证文献5

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部