形式等效性检查

一般来说，功能等价有很多种可能的定义，包括不同抽象层次和不同时序细节粒度之间的比较。

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

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

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

理论上，逻辑合成工具保证第一个网表在逻辑上等同于RTL源代码。在这个过程中后来对网表进行更改的所有程序，理论上也要确保这些更改在逻辑上等同于以前的版本。

实际上，程序会有缺陷，做出RTL到最终磁带输出网表的所有步骤都没有错误地执行的假设将是一个重大风险。此外，在现实生活中，设计师通常会对网表进行手动更改，通常称为工程变更单(Engineering Change Orders，简称ECo)，从而引入一个主要的额外错误因素。因此，不要盲目地假设没有出错，需要一个验证步骤来检查最终版本的网表与设计的原始描述(黄金参考模型)的逻辑等价性。

历史上，检查等价性的一种方法是使用最终的网表重新模拟为验证RTL的正确性而开发的测试用例。这个过程称为门级逻辑模拟。然而，这方面的问题是检查的质量只和测试用例的质量一样好。此外，众所周知，门级模拟执行缓慢是一个主要问题，因为数字设计的规模继续呈指数级增长。

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

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

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

• 二进制决策图，或称BDDs：一种专门的数据结构，旨在支持布尔函数的推理。BDD因其高效性和多功能性而广受欢迎。
• 合取范式可满足性：SAT解算器返回一个命题公式变量的赋值，如果这样的赋值存在的话，该赋值满足它。几乎任何布尔推理问题都可以表示为SAT问题。

EDA逻辑等效性检查(LEC)领域的主要产品有：

• 明导国际公司的FormalPro
• 明导国际公司的Questa SLEC
• 益华电脑股份有限公司的Conformal
• 益华电脑股份有限公司的JasperGold
• 新思科技的Formality
• 新思科技的VC Formal
• OneSpin Solutions 公司的360EC
• ATEC的ATEC

• 重定时电路的等效性检查：有时将逻辑从寄存器的一边移到另一边是有帮助的，这使得检查问题变得复杂。
• 顺序等价检查：有时，两台机器在组合层次上完全不同，但如果输入相同，应该给出相同的输出。典型的例子是两个相同的状态机，状态编码不同。因为这不能归结为组合问题，所以需要更通用的技术。
• 软件程序的等价性，即检查两个取N个输入并产生M个输出的定义明确的程序是否是等价的：从概念上讲，你可以把软件变成一个状态机(这就是编译器的组合，因为计算机加上它的内存形成了一个非常大的状态机)。)然后，理论上，各种形式的属性检查可以确保它们产生相同的输出。这个问题甚至比顺序等价检查更难，因为两个程序的输出可能出现在不同的时间；但是这是可能的，研究人员正在努力。