随着集成电路的设计规模越来越大、复杂度越来越高,产品上市时间却越来越紧迫,集成电路的验证变得越来越困难。2003年度的国际半导体技术发展报告指出,验证已经成为集成电路设计流程中的最大瓶颈。传统的模拟验证因其测试周期长、不能完全覆盖,已经不适合当前对集成电路验证的需求。形式化验证其原理是使用严格的数学推理来证明一个系统满足全部或部分规范,从而提高了验证的正确率,保证了市场需求。另外,它作为对传统基于模拟验证方法的补充,日益引起人们的关注。本课题在较为全面、深入地研究和总结国内外形式验证技术研究成果的基础上,对当前主流形式化验证方法中的推广化符号轨迹赋值(GSTE)验证方法进行了深入的研究和扩展,以期进一步减少伪报错现象,提高GSTE验证方法在集成电路验证中的正确性。本课题在研究方法上,首先,针对符号轨迹赋值(STE)验证方法的基本理论和技术,详细分析其优点和不足。对STE验证规范做出的图形化扩展和断言图,以及基于断言图的验证算法做认真的论证和分析。然后,分析GSTE验证方法,比较STE和GSTE的优缺点。进一步分析由于GSTE继承STE的抽象行为,而带来的伪报错问题产生的原因。在以上学习和分析的基础上,本文提出GSTE中SMC算法的改进算法,并通过验证平台FORTE对改进后的算法进行编码实现和验证。结果显示,在降低伪报错和查错方面都有较大改良和提高。另外,在不熟悉电路的情况下,进行集成电路验证时,可以通过使用GSTE中改进的SMC算法来验证电路的正确性。若非常熟悉本电路的设计,也可以按照回路进行手动扩展。同时,针对验证工具的自动化程度,本课题创造性地提出并设计了自动插入故障容错结构工具。在实际的某个电路设计流程中,如果验证结果返回为错误,对于没有参加本电路设计的人员来讲,发现错误并改正错误将是非常困难的。大部分电路设计的修改和优化,只是涉及电路部分结构的变化。如何能更有效、更准确地给出问题所在,是保证验证电路设计正确性的首要问题。