随着集成电路的规模增长、复杂度的日益提高，使用传统的基于模拟的方法进行验证已经无法满足开发大型硬件系统的需要。作为模拟验证方法的补充和完善，形式化验证方法使用数理逻辑来对系统进行建模和推理，进而严格地证明系统是否满足特定的设计规范。形式化的验证方法的优点在于它是完备的，不会遗漏掉边角情况。形式化验证方法是现代集成电路系统开发中必不可少的验证手段，对其加以进一步的研究，具有重要的意义。形式化验证技术主要包括模型检测(模型检验)、定理证明，以及等价性验证。本文研究的主要内容是针对组合电路的等价性验证。在等价性验证这个问题上，之前大多数相关的工作都是使用二叉决策图(BDDs)以及其它布尔表示形式来形式化和求解问题。这些方法都是基于位级的(bit level)，必须将系统转换到一位一位的布尔变量表示。而实际的算术电路中包含了字级的(word level)算术操作，转换过程会将设计中的这些高层规格说明信息丢失。为了克服这个缺点，以充分利用高层的信息，字级的证明方法相继出现了。比如字级决策图(WLDD)，带权值的广义表(WGL)，以及可满足性模理论(SMT)。利用可满足性模理论可以有效地处理包含字级的算术操作以及位级的布尔逻辑的设计的验证问题。本文提出一种使用基于字级的约束求解器判定两个组合电路是否等价的方法。首先，使用前端的词法和语法分析程序读入待验证的参考和实现电路，经过细化解析之后，提取各自的形式化模型。然后，由这两个模型满足的约束关系构造出联接电路(Miter)并交给后端的SMT求解器。我们通过使用静态单赋值形式提取Verilog程序的形式化模型，并结合基于字级的约束求解器STP，实现了针对Verilog组合电路的等价性验证工具。实验结果表明该方法可以有效利用字级的信息，并能有效避免内存爆炸问题。在实际待验证的两个电路中，通常存在一些内部等价点。基于结构的组合电路等价性验证方法在两个电路中寻找出这种结构相似性关系，然后利用这些信息简化验证问题。其中的一种基于结构的方法就是在电路的内部引入割点(cut-points)。通过将一部分子电路替换成割点，也就是把它看成是电路的输入，然后使用这些割点组成的集合重新构造电路，使得电路的表示形式大大减小，从而降低内存的使用，提高等价性验证工具能够验证的规模。这个化简的过程相当于将原始电路对应位置的取值放宽了，所以，如果化简之后的电路等价，则原始电路等价。否则，我们可以得到一组反例，也就是化简之后的电路的输入的赋值组合。如果原始电路在这些位置能够取到这组值，则原始电路不等价。否则，说明这个反例是假的。原始电路等价，而化简之后的电路不等价，这就是误判问题。在基于割集的等价性验证方法中，误判的发生是很常见的。一种消除误判的方法是选择一部分割点，将它替换为原来的子电路。经过若干次这样的迭代，直到证明出电路等价，或者反例是真的，也就是电路不等价。本文提出了一种当误判发生时，选择还原的割点的策略。通过不可满足核找出误判发生的根本原因，也就是找出导致误判的一组割点的集合，只还原这些割点，从而减少无关的割点的还原，以及迭代的次数。