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

《基于高阶逻辑系统hol的数字硬件形式化验证》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、西安电子科技大学硕士学位论文基于高阶逻辑系统HOL的数字硬件形式化验证姓名：林立申请学位级别：硕士专业：计算机应用技术指导教师：裘雪红;韩俊刚20050101摘要本文简单介绍了形式化方法的起源、发展、关键技术，并与传统的基于模拟的验证方法进行对比，分析它的优点和不足。对数字硬件形式化验证技术进行了分类，模型检测，定理证明和等价性检验。本文重点是基于HOL定理证明器的验证。为使用HOL系统，简单介绍函数式编程语言MOSCOWML，该语言是HOL系统的元语言。我们详细介绍了该定理证明器所支持高阶逻辑。分析了HOL系

2、统的逻辑建立过程，常用的理论库和重写策略。特别分析了HOL系统的证明方法及前向证明和目标制导这两种方法。作为上述理论的实际应用，重点给出了RSA数字硬件的一个形式化验证实例。首先介绍如何利用HOL验证RSA算法的正确性。然后详细介绍如何用HOL系统验证硬件设计的正确性。通过严密的思维和机器的辅助在严格的逻辑系统的基础上进行的证明可以提高设计的可靠性，进一步加强了RSA算法和硬件实现的正确性的信心。同时培养我们的科学态度和利用数学工具分析和解决问题的能力。关键字：HOLRSAML形式化验证AbstraetThep

3、aperdiscussesissuesincludedevelopmentmethodandoriginsofformaltechnology．Comparedwithsimulationandemulation，wediscusstheadvantagesanddisadvantagesofthismethod．weclassifydigitalhardwareformalverificationasequivalencechecking，modelcheckingandtheoremprovingandwe

4、focusontheoremprovingwithHOL．WeintroducetheprogramminginMOSCOWMLthatisafunctionalprogramlanguage．ItismetalanguageofHOLsystem，HOLsystemiswidelyusedintheworld．andHOLsystemisoneofthemostreliabletheoremprovingsystemforverifyinghardware．Weshowthelogicofthesystem，

5、commonly-usedtheory,rewritetactics，forwardproofandgoaldirectedproof．Asanpracticalapplication，WegivetheprocessofformallyveilfyingRSAdigitalhardware．formalverifytechniqueisaaccessorialtestingmethod．Byusingrigorousthoughtandlogicreasoning，ItCanimprovereliabilit

6、yofdesignofahardwaresystem，Keywords：HOLRSAMLFormalverification创新性声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以注明和致谢中所罗列的内容以外，论文中不包含其他人已经发表或撰写过的研究成果；也不包含为获得西安电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均己在论文中作了明确的说明并表示了谢意。申请学位论文与资料若有不实之处，本人承担一切相关责任。本

7、入签名：!奎童日期：主!堡主：!：!扩关于论文使用授权的说明本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究生在校攻读学位论文期间论文工作的知识产权单位属西安电子科技大学。本人保证毕业离校后，发表论文或使用论文工作成果时署名单位仍然为西安电子科技大学。学校有权保留送论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分内容，可以允许采用影印、缩印或其他复印手段保存论文。(保密的论文在解密后遵守此规定)本人签名：i查童日期：量型至：!．!￡导师签名塞窒i二日期：兰!：篁：!：：!绪论当今

8、微电子技术的发展，使得含有数百万门的集成电路已经能够大批量地生产出来，真正的系统芯片(SystemonChip)正在成为现实。但是如何正确她设计这些复杂的超大规模集成电路的问题还没有解决。可以说集成电路制造的能力超过了集成电路的设计能力。为了充分发挥投资惊人的集成电路生产线的生产能力，需要更多的设计者及时地提供大量复杂的设计。另外，计算机技术和通讯技术的高速发展，使得数字系统渗透到整个