Coudert等首先研究了确定性有限自动机的等价性验证问题。给定两个自动机，将其并联构成异或模型机A×B，然后从初始状态出发，采用宽度优先的搜索策略，计算该模型机所能到达的状态集合。通过比较输出响应，即可判定两个电路的等价性。BDD用于表示状态集合、状态转换图以及输出函数。其电路同样是采用前面提到的转换函数向量来表示。等价性的验证过程及其内部子过程与模型检验中极为相似，如用BDD表示状态转换图，求次态，以及求可到达集合等操作。这种方法的主要问题也是状态空间爆炸，对于大型设计就不能进行验证。因此，模型验证中这些问题的一些改进方法，都可以用在等价性验证中。例如，O.Coudert就提出，可以用一个统一的框架实现时序电路的两种验证类型：性质验证和等价性验证。方法就是在建立了该模型机之后，将等价性要求用基于时态逻辑的CTL描述，再采用模型检验方法进行性质验证。
　　S.Y.Huang 等提出了一种改进方法。这种方法结合了BDD和测试码自动生成方法ATPG的优点。采用时序ATPG技术，可以检测出两个时序电路中等价的触发器对，等价的内部信号对等。然后，利用这些等价的信号对简化异或模型机，最后对简化的问题进行验证和判别。这种方法可以验证具有数百个触发器的电路。
　　S.Devadas等在1988年提出了在不同抽象级别描述的时序电路的等价性验证问题。描述级别可以是寄存器传输级，或者是逻辑级。算法的基本思路如下：从RTL级和逻辑级分别提取出有限状态机的状态转换图STG；然后比较二者是否等价。在提取逻辑级的STG时，利用从第一个STG中获得的"不管"（don't care）信息，可以减少第二个STG的状态数和边数，从而降低验证的复杂度。但是由于其等价性判别方法是一种状态枚举的方法，因此，所能验证的规模很小。
　　等价性验证目前仍然是需要研究的问题。尤其不同级别的等价性验证问题，目前的方法还不是很有效。主要问题是从较低级别的功能抽象还是一个大问题。