随着集成电路设计技术的发展，芯片的设计越来越复杂。如何保证设计的功能正确，这是验证工程师所面临的一个严峻问题。由于集成电路规模增大，采用传统仿真(Simulation)验证方法进行功能验证的复杂度呈指数级增长，而完全形式化(Formal)的方法目前难以处理百万门以上的复杂设计，这使得集成电路设计能力和验证能力之间的差距越来越大。为了缩短这个差距，将仿真与形式化相结合的半形式化(Semi-Formal)验证方法成为目前国内外科研机构以及EDA厂商研究的热点。本文所做的工作也主要是在这方面的一些尝试。 龙芯2号是我国自主研发的高性能通用处理器，其设计十分复杂。为了对它进行充分的验证，我们也希望从可以半形式化的角度进行。为此，我们在结合Cadence SMV和NuSMV两个形式化验证工具的基础上实现了一个半形式化的验证原型系统。该半形式化验证系统核心包括设计模型化、验证规范描述、形式分析算法、初始状态选择四个方面。首先，将需要验证的设计模型化为Kripke结构，并以SMV语言形式在计算机中表示。其次，验证规范通过可计算树逻辑(CTL)或线性时态逻辑公式(LTL)表示出来。然后采用了基于SAT—BMC的模型检验方法作为半形式化验证系统的形式化分析引擎。最后在初始状态迁移方面可以采用仿真的方法，也可以直接初始化。 本文还根据IEEE—754标准，完成了一个部分功能的基准乘加部分部件描述。在此基础上，对龙芯2号的重要功能部件——浮点乘加部件(FMAF)完成了初步的验证。此外，还通过插入错误的方法，比较了传统仿真方法和半形式化的方法，发现基于SAT—BMC的半形式化方法在寻找错误所需的时间和稳定性方面都拥有巨大的优势。获取的这些有意义的结果，将为组内进一步开展半形式化验证工作提供了一些参考。