随着IT业的不断发展，集成电路产业增长迅速。而随着芯片复杂度的不断增加，设计出错的可能性越来越大，因而验证越来越重要，而验证新产品设计正确性的困难程度也在增长。但是传统的模拟和测试方法已经很难帮助设计人员开发出一个没有错误的完整设计来。除了模拟和测试外，形式化验证技术是一个非常有吸引力的方法，它能为设计无错误的产品提供保证。等价性验证是目前集成电路设计验证中应用最为广泛的形式化方法，其核心目标是验证两个设计模型之间的功能等价性。从整个数字系统的设计流程看，等价性问题几乎存在于每个上下相邻的设计层次中，此外在相同层次设计间做等价性验证的也很多。由于数字系统的复杂性和专业性，以及电路设计人员的专业需求，要想完成一个具有灵活性、可靠性、可扩展性的集成电路等价性验证系统，系统架构以及核心引擎则成为最关键的两个问题。本论文正是针对上述问题，以集成电路等价性验证系统的系统架构为主要的研究内容，在深入分析集成电路等价性验证原理的基础上，对系统架构和核心引擎算法作了创新性和探索性研究。主要内容为：1．详细研究了集成电路形式化验证技术。2．详细研究了集成电路等价性验证的原理。3．详细分析了基于SHELL引擎所实现的集成电路等价性验证系统的系统架构。4．详细分析了基于ATPG算法所实现的集成电路等价性验证系统的核心算法引擎。