形式上的等效检查

形式上的等效检查过程是电子设计自动化（EDA）的一部分，通常在数字集成电路的开发过程中使用，以正式证明电路设计的两个代表表现出完全相同的行为。

一般来说，功能等效性有多种可能的定义，涵盖了不同抽象层次和不同粒度的时序细节之间的比较。最常见的方法是考虑机器等效的问题，它定义了两个同步设计规范的功能等效，如果按时钟计算，它们对任何有效的输入信号序列产生完全相同的输出信号序列。微处理器设计者使用等效检查来比较为指令集结构（ISA）指定的功能和寄存器传输级（RTL）的实现，确保任何程序在两个模型上执行都会引起主存储器内容的相同更新。这是一个更普遍的问题。

在等价检查程序中，有两种基本技术用于布尔推理。二进制决策图，或称BDDs。一种专门的数据结构，旨在支持布尔函数的推理。