随着信息产业的发展，超大规模集成电路和数字系统几乎占据了我们生活的所有领域。而且，由于芯片设计复杂性与日俱增，新产品的功能验证难度也逐渐加大。由于这些原因，在设计阶段早期发现错误显得十分必要。因此，开发形式化验证技术来处理那些或许会引起功能不正确的设计阶段是非常重要的。等价性验证是形式化验证方法之一，它主要解决验证两个电路是否功能等价的问题。现在电路设计经常包含某些功能未知的模块，这些模块被称作黑盒。为了在早期阶段发现设计错误，我们对带黑盒的实现电路进行等价性验证。本文主要研究了集成电路的等价性验证理论及其在带黑盒电路上的应用，进而提出一种基于逻辑锥分割和SAT的带黑盒电路的等价性验证方法。主要包括以下三方面的内容：1．等价性验证：等价性验证技术证明两个被给定电路具有相同的功能。例如，一个优化的设计与其早期版本是功能等价的。在验证过程中，验证方法被分为两类：(1)符号方法，(2)增量方法。符号方法是指依赖于使用BDD符号技术的那些方法；增量方法是指在验证中，开发两个电路的结构相似性。2．带黑盒的等价性验证：在假设规范电路和带黑盒的实现电路具有组合性质的基础上，提出带黑盒的等价性验证方法。这些方法包括Local Check，Output Exact Check和Input Exact Check。使用这些方法相继地增加了算法的准确性和复杂性。3．一个有效的带黑盒电路的验证方法：我们提出了一种基于逻辑锥分割和可满足性的检验算法。根据“分而治之”的方法，把电路划分成若干子电路，使用符号模拟技术对黑盒的输出进行未知约束，然后对子电路的合取范式进行可满足性验证。这种方法增强了算法的错误检测能力，通过在ISCAS’85基准电路和10个简单组合电路上得到的两组实验数据表明了此算法的有效性和可行性。