形式验证一般分为两种：
　　1. 等价性验证：等价性验证主要指验证两个方案之间的等价性，一般用于底层验证，如逻辑综合前后方案的验证。在进行不同描述层次的等价性验证时，需要解决如何从低层描述抽象出有用信息，进而与高层设计方案比较等问题。
　　2. 性质验证：性质验证指对一个实现方案，不是去验证它所有的行为，而是验证它是否满足某些规则或性质。性质验证可以用于高层，如行为级验证。性质验证所用的规则和性质需要用户或设计人员给出，这就存在要验证多少性质才算足够的问题。
　　
　　等价性验证和性质验证都属于功能性的验证。等价性验证往往是针对两个电路描述证明他们在功能上是等价的。比如逻辑最小化后与原电路等价，对电路结构作局部修改后需证明与原电路等价，从较高级别的描述综合为较低级别的描述，也需要证明其所实现的电路与原来的描述等价，例如行为级到寄存器传输级，寄存器传输级到门级。

　　对组合电路来说，不存在状态寄存器，其输出值Z[t]为输入向量X[t]的函数，而不依赖于前面的输入值X[t-i], ( 1≤ i≤ t )。这时只需要对每个输入向量证明其输出向量相同。
　　在组合验证领域中出现的大多数方法大致可以分为两类。
　　(1)转换为单一抽象模型比较。C^A和C^B的输出布尔函数都转化为某一种单一形式。通过对这种单一表示的结构进行比较得出其功能等价的结论。在最坏情况下，布尔函数的正则表示随输入个数指数增加，其过大的内存需求限制了一般布尔函数的验证能力。
　　(2)利用测试输入向量进行验证。探寻使两个电路具有不同输出值的输入测试向量。若不存在这样的测试向量，则电路在功能上等价。在最坏情况下，这种方法需要穷举所有可能的输入测试向量，使得由于运行时间问题而限制了一般电路网络的验证能力。
　　成功的系统中用第一类方法较多。IBM的SAS(Static Analysis System)是基于类似于二叉判决图BDD(Binary Decision Diagrams)的方法的验证大型逻辑设计的程序，成功地应用于计算机设计中。
　　还有一种比较组合函数的基本方法是通过散列(Hash)技术将布尔函数映射到整数值的概率方法。这种方法降低了计算复杂度，但由于是多对一映射，会出现将不等价的电路识别为等价电路的问题。本节主要介绍利用二叉判决图验证组合电路的等价性问题。