当前集成电路发展日新月异,硬件电路的规模也随着摩尔定律在不断增加,硬件验证作为硬件设计的重要组成部分,也成为人们的研究热点。传统的验证手段主要有模拟、仿真等,但这些方法都有其局限性,于是研究者将形式化手段用到了硬件电路的验证上,就有了形式化验证技术。另一方面,随着半导体工艺水平不断提高,为了满足集成电路市场对芯片的成本、开发周期等要求,芯片设计已经逐渐走向SoC开发。SoC设计离不开IP库,其中IP软核又是被用的最广泛的形式,所以对IP软核需求也越来越多。同时,由于开发者大都需要对IP软核进行功能验证,这会拉长SoC的开发周期,于是本文提出了一种基于证明器验证方案,从而减少IP软核使用者的检查IP功能的时间。本文使用Coq平台,构造了一个硬件电路的逻辑模型,并建立了从RTL到Coq语言的转换规则,使得IP提供方可以根据需求规格书进行RTL代码的功能证明,然后IP使用者可以使用Coq工具快速检查功能证明的正确性,从而可以使得IP使用者缩短开发SoC的周期。本文还使用一些经典的同步电路根据我们制定的转换规则进行转换得到一系列假设,并根据相应的电路提取需要证明的定理,然后用转换得到的假设完成这些定理的证明。这些实验的成功完成证明了该方案的可行性。再利用这些转换得到的代码和证明代码作为基准来保证以后版本的兼容性。最后本文对经典的8051单片机进行指令级的功能验证。我们将8051单片机的代码遵照转换规则做完整的转换,然后用Coq语言编写指令功能的定理,使用通过RTL转换得到的假设对指令功能定理进行证明。结果表明,8051单片机在本文的转换规则和硬件电路模型下能够进行指令级功能的验证。