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