VLSI技术的快速提高导致硬件设计复杂性增大,使得检查电路的正确性已经变成一项非常困难的任务。在后面的设计环节中或者等到产品完成后再纠正错误将会耗费更多的费用,因此,为了能避免高额的产品开发费用,设计中的早期错误检测变得越来越重要。传统的验证方法就是对设计进行穷尽的模拟,即建立一个模型,用软件或者硬件方法赋予输入大量的测试向量,然后把模型输出和参考模型的功能进行比较来达到验证目的。但是这种方法不能完全保证设计的正确性,尤其是在大规模电路设计中,模拟验证的时间更要花费几年之久,这是我们无法忍受的。作为传统的模拟验证方法的补充,形式验证越来越引起人们的关注,它是通过严格的数学推理来证明一个系统满足全部或部分规范。形式化验证能大大减小设计时间而且能对设计进行完全覆盖验证。它不用波形或者激励而是直接采用硬件描述的方式,这样能更快得到结果和探测错误。等价性验证作为形式验证方法的一种,常被用于验证综合后电路以及人工修改后的电路。等价性检查主要用于验证RTL和RTL之间,RTL和门级网表之间以及门级网表和门级网表之间的等价性。本论文对一些传统的组合电路及时序电路等价性验证方法进行了介绍、分析、比较、总结并在此基础上进行了拓展。主要内容包括以下几个方面:1、介绍了等价性验证方法所采用的主要引擎是BDD。BDD数据结构的主要优点是表达形式简洁,占用的内存较小,能验证规模较大的电路。2、结合模拟验证和形式验证的优点,提出混合验证方法。模拟验证方法能检验规模比较大的电路,但是对测试向量选取非常依赖而且不能完全覆盖;形式验证方法能进行完全覆盖,但是只能验证小规模电路。结合两者优点既能验证大规模电路又能对其进行完全覆盖。3、提出了随机仿真技术的模拟验证方法。其主要方法是对电路输入加测试向量并对电路结点进行逐一比较。与传统的模拟验证方法不同,本文中采用随机仿真的目的不是对电路进行完全模拟,而是对电路内部的一些结点和寄存器进行初步匹配。4、采用了结构相似性技术。逻辑电路进行综合后与原电路常常存在很多相似的结构,对于这些结构相似的电路我们可以对它们进行合并化简,从而减小电路验证难度。5、采用了割集和局部BDD验证技术。割集和局部BDD是等价性验证的重要方法,本文中利用随机仿真和结构相似性技术中得到的等价部分作为割集,建立从割集到输出的局部BDD进一步减小了验证难度。