随着硬件设计技术的不断发展,硬件的规模越来越大、越来越复杂,硬件设计的正确性成为人们研究的热点。传统的验证手段主要有模拟、测试和仿真技术,但这些手段都有一定限制的,人们把形式化验证方法应用到硬件设计上,产生了硬件的形式化验证技术。形式化验证方法运用数学方法表达系统的规范或系统的性质,并且根据数学理论来证明设计的系统满足设计的规范或具有所期望的性质。目前比较流行的形式化验证方法主要分为两类:可达性分析和演绎方法,各种等价性检验器、模型检测器属于第一种,定理证明器属于第二种。各种形式化方法都有它的优缺点,模型检测的优点是完全自动化,但存在空间开销大的问题。定理证明器理论上可以处理无限状态的系统,但由于是交互式的,因此对使用者的要求较高。 本文从形式化方法入手,简单介绍了形式化方法的起源、分类、意义,分析了它的优缺点。本文对剑桥大学开发的基于高阶逻辑的定理证明器HOL系统进行研究:元语言ML、HOL逻辑及HOL系统的证明方式等。随后对用HOL系统进行硬件验证和验证中的关键技术:抽象技术、层次化验证技术进行研究。最后作为上述理论的应用,运用HOL-4系统对硬件电路:带复位的奇偶校验器、CPU的重要组成部分算术逻辑单元设计正确性进行了形式化验证,给出了实验结果。