形式等效性检查

形状等效性检查过程是电子设计自动化 (EDA) 的一部分，通常用于数字集成电路的开发，以正式证明电路设计的两种表示形式表现出完全相同的行为。

一般而言，功能等效性的可能定义范围很广，涵盖不同抽象级别和不同粒度的时序细节之间的比较。

• 最常见的方法是考虑机器等效性问题，它定义了两个同步设计规范在功能上等效，前提是它们逐个时钟地为任何有效的输入信号序列产生完全相同的输出信号序列。
• 微处理器设计人员使用等价性检查来比较为指令集架构 (ISA) 指定的功能与寄存器传输级 (RTL) 实现，确保在两种模型上执行的任何程序都会导致主内存内容的相同更新。 这是一个更普遍的问题。
• 系统设计流程需要比较事务级模型 (TLM)，例如用 SystemC 编写的模型及其相应的 RTL 规范。 这种检查在片上系统 (SoC) 设计环境中越来越受到关注。

数字芯片的寄存器传输级 (RTL) 行为通常使用硬件描述语言来描述，例如 Verilog 或 VHDL。 这个描述是黄金参考模型，详细描述了哪些操作将在哪个时钟周期内由哪些硬件执行。 一旦逻辑设计人员通过仿真和其他验证方法验证了寄存器传输描述，设计通常会通过逻辑综合工具转换为网表。 不要将等效性与功能正确性混淆，后者必须通过功能验证来确定。

初始网表在用作将逻辑元素放置到物理布局中的基础之前，通常会进行一些转换，例如优化、添加测试设计 (DFT) 结构等。 现代物理设计软件偶尔也会对网表进行重大修改（例如用具有更高或更低驱动强度和/或面积的等效相似元素替换逻辑元素）。 在一个非常复杂的多步骤过程的每一步中，必须保持原始代码描述的原始功能和行为。 当最终流片由数字芯片制成时，许多不同的 EDA 程序和可能的一些手动编辑将改变网表。

理论上，逻辑综合工具保证xxx个网表在逻辑上等同于 RTL 源代码。 理论上，过程中稍后对网表进行更改的所有程序也会确保这些更改在逻辑上等同于先前版本。

在实践中，程序存在错误，假设从 RTL 到最终流片网表的所有步骤都没有错误地执行，将是一个重大风险。 此外，在现实生活中，设计人员通常会手动更改网表，通常称为工程变更单或 ECO，从而引入一个主要的额外误差因素。 因此，与其盲目地假设没有错误，还需要一个验证步骤来检查网表的最终版本与设计的原始描述（黄金参考模型）的逻辑等效性。

从历史上看，检查等效性的一种方法是使用最终网表重新仿真为验证 RTL 的正确性而开发的测试用例。 这个过程称为门级逻辑仿真。 然而，这样做的问题是检查的质量与测试用例的质量一样好。 此外，众所周知，门级仿真的执行速度很慢，随着数字设计的规模继续呈指数增长，这是一个主要问题。

解决这个问题的另一种方法是正式证明 RTL 代码和从中合成的网表在所有（相关）情况下具有完全相同的行为。 这个过程称为形式等价性检查，是在更广泛的形式验证领域下研究的问题。

可以在设计的任意两个表示之间执行形式等价性检查：RTL <> 网表，网表 <> 网表或 RTL <> RTL，尽管与前两者相比后者很少见。 通常，正式的等价性检查工具还会非常精确地指示两种表示之间存在差异的点。

在等价性检查程序中有两种用于布尔推理的基本技术：

• 二元决策图或 BDD：一种专门的数据结构