基于高阶逻辑系统HOL的数字硬件形式化验证

发布时间：2021-04-21 02:43

　　本文简单介绍了形式化方法的起源、发展、关键技术，并与传统的基于模拟的验证方法进行对比，分析它的优点和不足。对数字硬件形式化验证技术进行了分类，模型检测，定理证明和等价性检验。本文重点是基于HOL定理证明器的验证。为使用HOL系统，简单介绍函数式编程语言MOSCOW ML，该语言是HOL系统的元语言。我们详细介绍了该定理证明器所支持高阶逻辑。分析了HOL系统的逻辑建立过程，常用的理论库和重写策略。特别分析了HOL系统的证明方法及前向证明和目标制导这两种方法。作为上述理论的实际应用，重点给出了RSA数字硬件的一个形式化验证实例。首先介绍如何利用HOL验证RSA算法的正确性。然后详细介绍如何用HOL系统验证硬件设计的正确性。通过严密的思维和机器的辅助在严格的逻辑系统的基础上进行的证明可以提高设计的可靠性，进一步加强了RSA算法和硬件实现的正确性的信心。同时培养我们的科学态度和利用数学工具分析和解决问题的能力。 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：69 页

【学位级别】：硕士

【文章目录】：
绪论
第一章 数字硬件形式化验证概述
    1.1 形式化
    1.2 形式化的方法
    1.3 形式化的发展
    1.4 硬件形式化描述
    1.5 硬件形式化验证的过程
    1.6 定理证明器
第二章 HOL系统
    2.1 ML语言的介绍
    2.2 HOL系统
第三章 RSA加密算法的形式化证明
    3.1 RSA算法
    3.2 RSA的安全性
    3.3 RSA的现状和前景
    3.4 RSA算法正确性的形式化验证
第四章 RSA数字硬件的形式化验证
    4.1 VHDL语言简介
    4.2 RSA数字硬件的实现
    4.3 模和同余的转换的形式化证明
    4.4 模乘运算模块的形式化验证
    4.5 加密模块的形式化验证
    4.6 证明思路的总结
    4.7 验证的结果
结论
致谢
参考文献
作者在读期间的研究成果
附录A 重要定理证明对策清单
附录B RSA数字硬件VHDL程序清单


【参考文献】：
期刊论文
[1]基于高阶逻辑的硬件验证方法[J]. 霍红卫,韩俊刚.  计算机学报. 1993(10)



本文编号：3150895