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