基于形式化方法的Booth乘法器可靠性研究

发布时间：2017-09-30 05:09

  本文关键词：基于形式化方法的Booth乘法器可靠性研究

  更多相关文章： 形式化方法 定理证明 乘法器 Booth算法 HOL4

【摘要】：由于超大规模集成电路的快速发展,系统的可靠性验证已经成为人们研究的重点。乘法器作为高性能微处理器中的核心运算部件,对它的可靠性进行验证是必不可少的一个环节。本文采用定理证明方法对二阶Booth乘法器的可靠性进行了研究,并在定理证明器HOL4中进行了相关的验证,主要完成的工作包括：首先介绍了形式化方法的基本概念,重点说明了定理证明方法以及定理证明器HOL4系统,其中包括HOL系统的发展历史、建模语言和证明方法等。其次形式化分析了二阶Booth算法的实现和规范,并在HOL4系统中完成了该算法的实现和规范的形式化建模；针对二阶Booth乘法器的结构特点,使用形式化方法详尽地分析了Booth编码模块、压缩模块和最终求和模块的实现和规范,并在HOL4系统中完成了这三个模块的实现和规范的形式化建模。接着在压缩模块和最终求和模块的基础上,层次化分析了组合模块的实现和规范,并在HOL4系统中完成了它的实现和规范的形式化建模。最后在HOL4系统中,利用建模过程中定义的定理以及内嵌的公理、推理规则等完成了对Booth算法、Booth编码模块、压缩模块、最终求和模块以及组合模块的形式化验证,不仅证明了二阶Booth乘法器的可靠性,也展现了HOL4系统在硬件验证与算法验证上的强大功能,对HOL4系统的进一步发展起到了促进作用。
【关键词】：形式化方法 定理证明 乘法器 Booth算法 HOL4
【学位授予单位】：北京化工大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP332.22
【目录】：

• 摘要4-6
• ABSTRACT6-12
• 第一章 绪论12-18
• 1.1 研究背景及意义12-13
• 1.2 国内外研究现状13-15
• 1.3 课题研究的主要内容15
• 1.4 本文组织结构15-18
• 第二章 形式化方法18-32
• 2.1 形式化方法简介18-19
• 2.2 模型检测19-20
• 2.3 等价性检测20-21
• 2.4 定理证明21-22
• 2.5 HOL4系统22-31
• 2.5.1 HOL系统的历史发展22-23
• 2.5.2 ML语言23-25
• 2.5.3 HOL逻辑与类型25-27
• 2.5.4 HOL的证明方法27-31
• 2.6 本章小结31-32
• 第三章 二阶Booth乘法器的形式化分析与建模32-52
• 3.1 Booth算法32-33
• 3.2 二阶Booth乘法器的电路实现33-40
• 3.2.1 Booth编码模块35-37
• 3.2.2 压缩模块37-39
• 3.2.3 最终求和模块39
• 3.2.4 组合模块39-40
• 3.3 二阶Booth乘法器的形式化建模40-50
• 3.3.1 Booth算法的形式化建模40-42
• 3.3.2 Booth编码电路的形式化建模42-43
• 3.3.3 压缩模块的形式化建模43-44
• 3.3.4 最终求和模块的形式化建模44-48
• 3.3.5 组合模块的形式化建模48-50
• 3.4 本章小结50-52
• 第四章 二阶Booth乘法器的可靠性验证52-70
• 4.1 Booth算法的形式化验证52-55
• 4.2 Booth编码模块的形式化验证55-61
• 4.3 压缩模块的形式化验证61-63
• 4.4 最终求和模块的形式化验证63-65
• 4.5 组合模块的形式化验证65-68
• 4.6 本章小结68-70
• 第五章 总结与展望70-72
• 5.1 总结70
• 5.2 展望70-72
• 参考文献72-76
• 致谢76-78
• 研究成果及发表的学术论文78-80
• 作者与导师简介80-81
• 附件81-82

【参考文献】

中国期刊全文数据库 前3条

1 朱一杰,张曦,俞军;双字节Booth乘法器的优化设计[J];复旦学报(自然科学版);2005年01期

2 杨泽民;范全润;;硬件设计的形式化验证技术[J];太原师范学院学报(自然科学版);2007年02期

3 赵刚;赵春娜;关永;吕兴利;李晓娟;施智平;王瑞;叶世伟;;拉普拉斯变换微积分性质在HOL4中的形式化[J];小型微型计算机系统;2014年09期

中国硕士学位论文全文数据库 前1条

1 陈波;基于定理证明器HOL的硬件验证研究[D];兰州大学;2006年

，

本文编号：946295