数字集成电路因抗干扰能力强、集成度高等优势得到了快速发展并被广泛应用于人们的日常生活中。数字集成电路设计的核心是RTL级代码设计,即使用硬件描述语言（Hardware Description Language,HDL）描述预期电路,但是HDL中只有部分语法结构能够被综合为后续硬件电路设计所需的网表文件,且不同厂家的综合工具所支持的可综合HDL语法结构也存在不同。而利用有限状态机（Finite State Machine,FSM）设计可综合的HDL代码这一方法,能够确保所实现的代码不仅可以被不同工具综合优化,而且还具有较高的稳定性和可靠性。因此,该方法成为设计可综合HDL代码的重要手段。然而随着所设计电路规模的不断增大以及功能的愈加复杂,验证HDL代码是否满足用户需求即FSM的功能和约束也变得越发困难。目前大多用于验证的仿真方法,不仅涉及到的仿真工具颇为昂贵,而且存在验证效率低、工作量大等问题,而形式化验证方法可以通过严格的数学逻辑证明软硬件系统的安全性与可靠性。为解决上述问题,本文提出了一种基于形式化验证方法的Verilog程序对FSM的可满足性验证方法,根据该方法设计实现了一个运行时验证工具集FVRVT（FSM and Verilog Runtime Verification Toolset）,并通过多个示范实例证明了所提方法和工具集的可行性和有效性。本文的主要工作有以下几点:（1）通过研究FSM的组成结构,针对目前还没有特定手段对FSM进行性质提取这一问题,提出了基于FSM的性质提取方法,并且详细地阐述了如何从FSM中提取约束性质以及如何从FSM的一个状态序列中提取功能性质,同时说明了将所提性质描述为命题投影时序逻辑（Propositional Projection Temporal Logic,PPTL）公式的方法。（2）为了确保建模仿真验证语言（Modeling Simulation and Verification Language,MSVL）与Verilog具有相同语义,本文还对支持验证需要的V2M转换器进行大量测试,发现其存在的多个问题。在定位每个错误产生的根源后,对原V2M转换器进行优化,实现了连续赋值功能和初始化语句转换功能,提出了新的模块实例化转换算法和拼接操作转换算法,解决了赋值语句问题和变量重复声明问题,从而确保优化后的V2M转换器能够生成与Verilog具有相同语义的MSVL程序。（3）在FSM性质提取方法和优化后的V2M转换器的基础上,提出了基于MSVL和PPTL的Verilog程序对FSM的可满足性验证方法。该方法一方面从FSM中提取出表示功能和约束的性质并描述为PPTL公式,另一方面把Verilog程序转换成语义相同的MSVL程序,从而将Verilog对FSM的可满足性问题转换为MSVL对PPTL的可满足性问题,这样通过MSVL程序与PPTL性质公式的运行时验证结果,即可判断Verilog是否满足FSM的功能和约束。（4）根据所提验证方法设计了一个运行时验证工具集FVRVT,该工具集通过利用V2M、UMC4M、MC编译器、iverilog和gtkwave等工具,实现了 Verilog程序对FSM的可满足性验证的完整流程。最后通过多个示范实例对所提方法和工具集进行检验,多个实例验证结果均表明,本文所提方法是可行且可靠的,并且实现的工具集能够完成Verilog程序对FSM的可满足性验证。