Formal equivalence verification 形式验证之等价验证 FEV 第8章

现在讨论FV的等价性，也叫形式等价性验证（FEV）或形式等价性检查（FEC），Synopsys公司的formality就是做等价验证的一款工具，是对组合逻辑做等价性检查。

FEV用来比较两个模型是否等效。一般是将说明文件（specification）和实施后文件（implementation）作比较：

SPEC一般是RTL级设计文件、未优化的原理图网表、参考模型或高级建模语言中的描述；
IMP通常是更具体、更精细的模型，进过其它工艺处理优化过的原理图网表实现。

一、要检查的等价类型

等价检查：

对于相同的输入，SPEC 和 IMP 的响应是一致
SPEC 对输入做出响应，IMP 应该也做出一样的响应

做等价验证是对关键点做比较，关键点可能包括：

Primary inputs
Primary outputs
State elements (latches and flip-flops)
Blackboxes
Cut points

上图说明FEV关键点和逻辑锥检查的基本概念，圈起来的是被比较的逻辑锥。

当前EDA工具常用的几个主要等价概念是：组合等价、序列等价和事务等价（transactional equivalence）。

1、组合等价

组合等价是EDA行业中最成熟的FEV技术，formality就是组合等价验证工具，很多IC设计公司的一项基本要求：比较RTL和netlist。

状态匹配模型中，SPEC中的每个状态元素（锁存器或触发器）对应于IMP中的特定状态元素，任何一对组合逻辑在逻辑上等价时，则称为等价。这两种设计中fanin锥中的对应状态元素在所有时间点都包含相同的值，且它们的每个锁存器或寄存器都被视为一个切点，验证只包括状态元素之间的逻辑。

EDA工具使用状态匹配，以保证网表中的每个状态元素都对应于RTL中的一个状态元素。使用状态匹配的FEV工具只需要分析布尔表达式，而不需要考虑值随时间的变化，因此，组合等价形式验证是现在大多数RTL–netlist逻辑检查器所使用的技术。由于RTL和netlist状态元素直接相互对应，不仅会比较输出，还会单独检查驱动每对对应状态的逻辑锥，以确保网表是RTL的真正实现。

如上图所示，关键点由输入输出接口和内部状态元素组成，比较的主要点是状态元素{F1,F3}、{F2,F4}和输出out。

只要两个模型中的每个内部和输出关键点都具有逻辑等价的组合驱动锥，那么这两个模型是等价的。

这种等价形式会有一些局限性。例如，如果希望实现重新编码FSM，使用不同的中间状态集最终生成相同的输出，会发生什么？如果不满足“组合等价在FSM中的应用，仅限于比较具有等价状态元素集的模型”这个条件，组合FEV工具将报告两个模型不等价。

2、序列等价

在一些供应商看来，序列等价也被称为周期精确等价（cycle-accurate equivalence）。使用序列FEV工具，不要求内部状态元素完全对应时，两个模型是否最终会基于一组等价的输入在同一时间生成相同的输出。因此，序列FEV工具可以处理上述重新编码的FSM情况。

一般来说，序列FEV被认为等同于之前讨论的形式属性验证（FPV），SPEC相当于一个大的参考模型。

与组合检查器不同，序列等价检查器可以验证具有通用功能的设计，但在以下方面存在差异：

State Representation
Pipeline depth
Interface timing and protocols
Resource scheduling and allocation（资源调度与分配）
Differences in data types
Clock gating and other power-saving features（时钟选通和其他节能功能）

3、基于事务的等价

这是序列FEV的另一种变形，在某些情况下，一个模型与另一个模型相比将是高度抽象的，其输出通常不会逐周期匹配，但某些定义明确的事务除外。等价性可以是在固定数量的RTL时钟周期之后，这可能表示事务，也可以是基于事务完成的完全不可预测的数字。因此，这个概念更通用，是所有等价模式的超集：没有组合或序列等价的模型可能仍然能够证明是基于事务的等价。

上图演示了基于事务的等价性检查的高级视图。

图8.2是典型设计的“交易空间”的概念视图，这一等价概念相当普遍，包含了前面描述的等价概念：

不假设RTL和系统级设计（SLM）完成一个事务所需的时间（或状态转换次数）相同
通过固定数量的RTL周期或某种“数据就绪”握手协议表示事务的结束
假设用户能够为RTL和系统级设计指定一组初始状态（将值部分分配给状态保持元素），这表示有效事务开始时的模型状态
假设用户能够为两种设计指定一组状态，这两种设计对应于事务的结束。

在事务结束时，比较两个设计的输出并进行检查，以确保两个设计的结束状态仍然满足状态不变量和约束。

如果设计变更涉及复杂的序列变更，而这些变更超出了序列FEV工具的能力，则可以使用基于事务的FEV对其进行验证。

基于事务的FEV工具是一种相对较新的FV类型，在EDA市场中还不是很成熟

二、FEV用例

目前EDA行业中最成熟的两种FEV流工具是RTL–netlist FEV和RTL–RTL FEV。

1、RTL — netlist FEV

逻辑综合（Logic synthesis，一种通过标准EDA工具将设计的RTL模型自动转换为晶体管级原理图网表的过程）在该行业已经是近20年的成熟过程。但逻辑综合这个过程很容易出现错误，有太多的转换发生，可能会以错误的方式更改网络列表，并使其定义与原始RTL中的预期不同的功能。这些错误可能是由于对合成工具的错误或不完整的用户说明、SystemVerilog或其他RTL语言的歧义和误解、错误记录的设计库或组件，或合成工具本身偶尔出现错误造成的。现在所有做逻辑合成的人都应该使用组合FEV工具，用于检查RTL是否与网络列表匹配。

图8.1中，两个电路都使用输入b之前两个周期的值计算输入a的NAND。

建立等价的第一步是映射两个电路之间的所有关键点，输入被映射成由相同的变量和分析值驱动，输出在形式上必须相等，但因为这是组合FEV，需要映射设计的所有状态元素。

组合FEV工具能自动映射，其中跨两种设计的key points会自动映射，包括接口信号、内部状态元素和任何黑盒，这通常是基于匹配名称和启发式的组合，例如寻找具有相应输入集的内部逻辑锥。

映射完成后，FEV工具执行实际验证，计算布尔方程并进行比较，以检查相应的关键点是否具有等效方程。

如上图所示，所有的信号匹配，尽管输出out信号的方程看起来不太一样，但是在替换相应的映射节点并使用德摩根定律展开后，在逻辑上是等价的。

在进行RTL-netlist FEV时，有时可能需要一些用户指导或特定指令来寻找某些类型的优化进行匹配，比如说手动匹配或加入一些约束条件。

2、RTL–RTL FEV

形式上确定RTL模型之间功能等价的能力，是在高性能设计中实践的物理感知前端设计中的关键促成因素。诸如参数化、定时修复、流水线优化、时钟选通和“chicken bit”验证等情况都可以使用FEV工具进行彻底检查。

1）参数化

大多数传统设计如：RTL最初对数据宽度、最大信息尺寸或线程数等参数进行硬编码。随着新项目计划在各种配置中使用设计，设计团队需要插入参数选项来代替RTL常量，这样的替换可能会涉及数百个单独的文件。

图8.4显示了针对各种市场的一系列平面设计的大量增殖，可以在设计上运行FEV，以非参数化代码作为SPEC，以参数化代码（默认参数）作为IMP。

一般可以通过组合FEV工具来处理，尽管在参数化伴随着状态元素中的相关结构更改时，可能需要使用序列FEV。

如果要用RTL模型中的参数替换常量，则应使用组合或序列FEV工具，以确保未更改逻辑。

2）序列修复——逻辑再分配

对于同步设计来说，修复关键时序（timing）路径都比较耗时，修复的常用解决方案是在不同的流水线级（pipeline stages）重新分配逻辑，但在修复时序问题时，会引入大量无意的功能性错误。运行FV可以轻松避免，确保设计保持其合理性，而不考虑跨管道（pipe ）的逻辑重新分配问题。

如图8.5所示，在第一个和第二个触发器之间有一条组合路径，将一些逻辑移过第二个触发器。重新分配该路径以修复冲突，最终将生成相同的输出，但该内部触发器的中间值会在计算的不同阶段出现。这两种设计不是状态匹配：虽然它们可能具有相同数量的触发器，但由于流水线（pipelines）中逻辑的重新分配，触发器的功能将不同。因此，此类检查首选序列FEV工具。

如果在RTL中跨管道级重新分配逻辑，使用序列FEV工具以确保没有更改逻辑。

3）序列修复——减少关键路径

如果修改管道状态（pipe stages）不是一个可行的选项，可以计算逻辑分成两部分，并通过并行触发器路径重定向其中的一部分，如图8.6所示。

一些商业组合FEV工具可以智能地处理此类情况，但有时需要用户干预才能进行适当的分析，但序列FEV能更好地处理这种情况。

4）管道优化

随着制造过程、算法和实现方法的逐渐成熟，通常可以减少管道深度。但有时定时修复和其他算法要求，在保留功能的同时添加额外的流水线（pipeline stage）。

根据重新优化流水线的情况，图8.7中的一个设计部分可被视为specification，另一部分可被视为implementation。

状态集已经改变，但端到端的功能没有受到干扰；应使用某种形式的FEV来验证这种变化。等价性检查需要定义两个模型之间的延迟差异，如果只是简单的差异，序列FEV工具应该能够验证，但如果更改很复杂，则需要一个基于事务的FEV工具。

5）Chicken bit 验证

Chicken bits，也叫作“失败比特”，是暴露给驱动的额外控制信号，以禁用硅中的一项功能。Chicken bits通常发生在项目后期修复bug，或者在最后一刻添加关键的新功能时。大多数稳定设计的修复程序都生成了Chicken bits，当它们无意中影响其他功能时，就会产生许多错误。验证Chicken bits可能很有挑战性，因为禁用一个功能在代码中通常和该功能本身一样具有侵入性。

图8.8说明了Chicken bits的典型实现，新分支向MUX提供信息，MUX在特定触发器逻辑的新旧实现之间进行选择。

保证设计变更正确性的一种方法是，在禁用新功能时，针对当前设计运行早期设计的FEV。有时，这可以通过组合FEV工具来完成，但在变更跨越多个状态元素的逻辑的情况下，通常需要顺序FEV。

如果插入Chicken bits以禁用某些新功能，在Chicken bits打开的情况下运行旧逻辑与新逻辑的组合或序列FEV，以检查当禁用新功能时，设计行为与原始设计是否真正匹配。

6）时钟选通验证

现代设计中，最常用的低功耗技术之一是时钟选通，在某些情况下关闭时钟以避免切换未使用的逻辑，从而降低总体功耗。如果一段逻辑没有正确关闭时钟，不正确的状态信号值和信号故障可能会传播并导致数据损坏。

在设计中插入时钟选通，使用序列FEV将设计与时钟选通打开和关闭进行比较，以确保时钟选通不会改变逻辑。由于时钟选通与状态元素的设计之间存在大量的交互作用，这类验证，序列FEV通常比组合FEV更成功。

三、运行FEV

首先选择要比较的模型，然后选择定义了主要验证任务的SPEC和IMP模型；处理关键点映射，可能需要定义一些假设和约束条件，最后调试FEV工具报告的任何不匹配。

1、选择模型

1）验证的模型

从RTL模型综合成网表的过程分为几个阶段，合成过程可能如下所示：

原始RTL：设计团队提供的RTL模型
预综合细化：详细RTL的Verilog表示，模块未经配置，并应用了各种用户合成指令
未优化的网表：第一次网表表示，逻辑上实现RTL，但不考虑后端因素
时序优化网表：为满足时间要求而进行优化的网表
Scan-Inserted Netlist：已插入扫描和调试功能的网表
功耗优化网标：进一步改进以添加隔离和保持单元，以及其他功耗方面的考虑。

最简单的过程是：运行FEV比较开始的RTL和最终功耗优化好的网表。在许多情况下，端到端流程会遇到复杂性问题。最简单的选择可能是拆分验证：根据中间网表验证RTL，然后根据最后一个网表验证中间网表。完整的端到端运行会产生一个重大的复杂性问题，而添加一个中间阶段并将工作分成两次运行会导致非常高效的执行。

如果运行RTL-RTL FEV来验证错误修复、重新执行流水线、时钟选通或相似场景，需要考虑是尝试一次验证一系列更改，还是可以获得RTL的中间版本，其中每个版本中都存在一种主要的更改类型，如果在较小的阶段验证更改，而不是进行一次完整的端到端运行，可以避免很多问题。

2）元件库

元件是实现基本逻辑功能的晶体管级设计，如与门、触发器或多路复用器，现在的综合工具从元件库构建网表，而不是直接生成晶体管级模型。元件隐藏晶体管级逻辑，并提供行为描述和逻辑Verilog，可在FEV工具中验证设计时使用。

RTL与netlist或netlist与netlist比较时，经常出现一个错误：包含库元件的完整晶体管级模型，并尝试验证这些完整的网表模型。这会导致复杂性提升，并且通常会根据内部元件实现细节生成额外的关键点。

如果执行RTL–netlist FEV，须使用已发布的元件库，其中包含已验证的行为规范，并加载元件库的行为表示。

2、关键点选择和映射

最简单的关键点选择类型是使用所有锁存器和触发器作为关键点，以及输入输出。

上图中红色圆圈中的为关键点。序列（sequential）等价工具中，唯一保证的关键点是模型输入和输出，提供内部关键点可以显著提高效率，并且可以解决以前不可行的等价问题。如果运行序列等价，应考虑潜在的关键点，尤其是试图验证更改模型的一个小区域时，而SPEC和IMP通常状态匹配。

1）定义映射

通常组合FEV工具能自动确定SPEC和IMP关键点之间的映射，但仍会有一些遗漏。可能是综合工具的命名约定混淆了FEV工具的映射算法，或者用户手动编辑了网表，并为某些节点指定了任意名称；也可能是序列FEV工具，默认情况下不会映射内部节点，但用户却确定了一大类希望工具映射的对应点。

为了处理这些情况，FEV工具提供了指定映射规则的能力，正则表达式告诉工具如何转换SPEC信号名称以匹配IMP名称。比如，综合工具可以更改括号中的数组引用，使用双下划线来分隔索引：RTL中的foo[12]可能会变成网表中的foo__12__。

要启用名称不同的等效节点之间的映射，可以向FEV工具提供如下指令：

add map rule [ __
add map rule ] __

2）状态否定

一种常见的可中断状态匹配的综合优化是状态否定，其中由于时序原因，信号在flip-flop的输入和输出端被反转。

如图8.10，有两个等价的设计，但在第二个设计中第二个触发器前后添加了反转，最终输出out是相同的。

一些FEV工具可以自动发现并创建反转映射，但在某些情况下用户需指定反转。在调试器中，需要查找包括不匹配的状态元素在内的、看起来有逻辑反转的情况的FEV验证结果，并将这些情况视为反转映射的候选。

如果RTL—netlist FEV中的内部信号不匹配，且通过一次反转而关闭，则这个信号是否定映射候选。但在基本输入和输出（primary input/output）信号上不适用 [因为它们的输入锥（用于输入）或输出锥（用于输出）在当前FEV运行中不可见]，除非确定否定的映射是正确的。

3）状态复制

某些由综合工具插入的定时修复通常需要状态复制（state replication），其中一个触发器被一组等效触发器替换。

4）不可到达点

设置关键点映射时可能会遇到另一个复杂问题：不可到达点。

不可到达点是一个状态元素，在逻辑上不能影响设计的任何输出，经常出现在RTL模型中（因为功能被禁用或删除，或重复使用的部分代码不再相关）。

不可到达点也可能出现在网表中，因为综合工具插入了一些只使用部分功能的标准库组件。组合FEV会在所有状态元素中分解逻辑，与设计的其他部分一样，这些不可到达点被确定为关键点，并可能导致报告未映射的关键点。

5）延迟映射和条件映射

RTL和网表之间的状态匹配比较时，上面讨论的映射复杂性主要是组合FEV运行中的问题。但如果运行序列FEV，IMP模型的输出关键点可能并不总是与SPEC模型的相应输出精确匹配。

模型的输出之间通常会有一些延迟，例如，如果比较一个非流水线模型和一个流水线模型，或者比较两个具有不同状态集的流水线模型，就会出现这种情况。FEV工具会提供指定某种延迟映射的方法，由流水线深度确定延迟后，输出应该进行对应。

也可能需要条件映射。例如，当存在有效操作时，SPEC和IMP的输出可能会相对应；但当操作无效时，就没有必要强制执行等价。

6）调试映射failures

在RTL—netlist FEV运行中尽最大努力解决上述所有问题后，SPEC和IMP中可能仍有一些未映射的点，没有明显的名字对应于另一个模型中的内容。

如果在映射所有关键点时遇到问题，首先查找与典型的综合网表优化或不可到达点相关的根本原因，然后查找基于名称的对应关系，并考虑在映射的附近点上运行部分验证以获得更好的提示。

3、假设和约束

假设和约束在FEV环境中比在FPV环境中容易，因为关键点映射过程隐含了一大类重要的初始假设：在SPEC和IMP模型中，假设任何逻辑锥的输入端对应的关键点等效，通常这些都是证明等价性所需的所有假设。

在一些情况下，可能需要其他假设或约束。

1）删除一些功能

在很多情况下，FEV运行的主要目的是检查：当删除某个新的或已修改的功能时，这两个模型在其他方面是等效的。要在其中一个模型中执行所需的删除，通常可以使用SVA假设或工具指令。例如，如果一个名为defeature的pin控制某个新功能是否处于活动状态，则添加一个假设，如

fev_feature_off: assume property (defeature == 1);

2）扫描（scan）（以及其他仅限于网表的功能）插入

当前硬件设计的一个共同特点是在综合过程中实现扫描链，这有时也被称为可测试性设计（DFT）。扫描链是一条长的串行路径，可以将任意内部状态导出到一组小的管脚上，这是观察设计内部状态所必需的，对于后期硅调试非常关键。根据扫描链的性质，状态的顺序高度依赖于设计的最终布局，与逻辑RTL层次结构无关。因此，扫描链很难在RTL中表示，大多数综合工具在综合过程中自动插入扫描链。

图8.12显示了扫描链插入的典型场景。

扫描逻辑不在RTL中表示，存在于网表中，因此在检查RTL–netlist等价性时必须禁用扫描逻辑。通常有一个简单的顶层机制来禁用扫描，如图8.12中示例中的sen信号；告诉FEV工具将sen信号保持在恒定的0值时，关闭扫描。

fev_scan_off: assume property (sen == 0);

如果在RTL –netlist FEV中发现大量不匹配，涉及与扫描或DFT相关名称的信号，检查是否正确禁用了模型的扫描；确定扫描条件，并为FEV工具提供适当的假设或指示以禁用扫描。

扫描问题可以被视为一个更普遍问题的具体案例，即使用RTL的面向方面编程（AOP），AOP对RTL的某些“方面”有一个外部规范，例如扫描、电源或调试，这在逻辑中没有直接表示。这些基于方面的行为，通过在综合的某个阶段自动插入RTL或网表，成为最终设计的一部分。

4、调试不匹配

调试工具报告两个模型不匹配的情况，驱动一对特定映射触发器或输出的逻辑在SPEC和IMP是不同的。大多数工具都提供用于调试的原理图或波形视图，当开始调试FEV不匹配时，应该从以下几点开始：

Sort by cone size（按锥的大小排序）：失败比较点的逻辑锥可能因复杂性而显著不同：非常简单的锥，可以一眼就完全理解逻辑视图；复杂的锥，有数百个节点。从最小的开始，调试会更有效率。
检查fanin锥的差异：大多数工具都提供获取fanin锥中关键点列表的方法，如果一对对应的节点不同、fanin有不同的关键点，这是差异根本原因。在某些fanin点上可能存在映射问题，可能是映射规则中编写得不好的正则表达式将错误的对设置为对应的，关键点差异可能表示缺少逻辑的关键部分，如扫描，要么需要忽略（如上所述），要么综合错误，表明存在真正的错误。
寻找共同的主题：如果有很多故障，且在查看第一个故障的fanin时没有发现任何明显的问题，那么查看其中的几个故障，看看是否有一种模式。
检查逆映射：如果成对的节点有相同的fanin锥和相似的逻辑，但值正好相反，则考虑是不是状态否定的情况，在这里需要指定逆映射。

上述问题适用于组合式和序列FEV。使用序列FEV工具时，还有一些其他问题需要考虑：确保已经检查了延迟或条件映射的需要。

序列FEV运行通常会遇到与多周期行为有关的故障，仍应该从上面的问题开始；但在大多数情况下，用于差异的调试技术还是类似于FPV调试。

四、FEV面临的其他挑战

1、锁存器/触发器优化

根据综合的网表验证RTL模型时经常出现的一个复杂问题是，这些工具可以在综合过程中优化一些设计，打破严格的状态匹配范式。这些常见的优化可以在组合FEV工具中通过简单的“重构”启发式处理，本质上是以逻辑合理的方式对内部表示进行黑客攻击，以恢复状态匹配。

图8.13显示了一个常数传播的简单示例，其中一个带有常数驱动器的触发器被一个简单常数替换，这在不改变功能的情况下减少了门计数。

大多数组合FEV工具可以自动检测和处理这种简单的优化。下面是其他一些此类优化比较的例子：

锁存器折叠：将两个相邻的锁存器组合成一个等效的触发器。
利用透明度（Exploiting transparency）：如果锁存器的时钟为常数1，则将其视为缓冲区。
反馈回路：在某些情况下，如果触发器的数据直接反馈到输入端，则将其视为锁存器。

如果综合流执行了这些优化，但用户没有向FEV工具提供处理它们的指令，那么在验证的RTL或网表端看到不匹配的状态关键点，它们无法映射到相应的点。

2、条件等价

在某些情况下，仅在特定条件下等价模型上运行FEV。例如，可能有一个模型包含不再使用的RTL功能，需要关闭；或者综合工具利用了用户提示，在某些无效输入条件下生成了一个与RTL逻辑不同的网表。

图8.14中描述了电路优化的一个例子，在a必须始终等于1的假设下，两条逻辑等价。

在FEV的早期阶段，检查FEV工具生成的初始反例，并确定定义等效性可能需要的假设，并生成所需的、已缺失的假设，像在FPV中一样。

在做组合FEV时，在状态元素的每一层添加假设，而不仅仅是在输入上。

如果用户给综合工具提供了说明规范，即一些约束：如特定的信号集是恒定的、等价的或相互排斥的，那么用户也应该为FEV工具提供类似的假设。

3、不在乎（DC）空间

Don’t Care space (DC space)是用户问题空间中没有定义行为的部分。例如，假设RTL中有这个代码片段：

case (myvec)
2’b00: out=0
2’b01: out=1
2’b10: out=1
Endcase

上述代码中并未指明myvec值为2’b11的情况。

在RTL-netlist FEV中，RTL是说明规范（specification）,netlist 是实施（implementation）。在RTL-RTL FEV中，标记为SPEC的模型是正确行为的定义，当且仅当IMP在所有合法实例（case）中生成与SPEC相同的输出时，才会认为IMP是正确的。

如何对待DC空间形成了两种设计之间的基本不对称：

SPEC：说明规范中的DC空间提供了一种实现选择：它基本上表明用户不关心这些情况下的结果。implementation为这些情况所做的任何事情都是正确的。
IMP：如果implementation模型中存在DC空间，这表明实现的逻辑不能提供确定性结果。如果实现定义的DC空间不是specification DC空间的子集，FEV工具将报告不匹配。

这种基本的不对称性，有可能在FEV工具中成功地证明模型A与模型B匹配，然后反转两个模型，并证明由于DC空间，模型B与模型A不匹配。在实际项目中，两个从同一RTL合成的网表，并且每个网表都经过形式验证，等同于该RTL，被FEV证明彼此不等价，这种情况如图8.15所示：

如果两个模型是从FEV中的一个常见模型不匹配中衍生出来的（并与之相反），则要仔细查看DC空间，如果比较从同一RTL模型合成的两个不同的网表，这尤其可能成为一个问题。

4、复杂性

FEV解决在已知最坏情况下需要指数时间的问题，因此容易出现复杂性问题：工具永远运行、超时或系统内存不足。在组合FEV中，状态匹配在大多数情况下降低了复杂性，但工具仍有可能无法验证大型逻辑锥。在序列FEV中，面临着与FPV模型相同的复杂性问题。

这里总结了一些处理复杂性的基本技术，特别适用于FEV环境，在面对FEV复杂性问题时首先考虑：

添加验证阶段：综合过程包含许多不同的阶段，例如未优化的网表、定时优化的网表和扫描插入的网表；使用中间阶段并将其拆分为一组较小的FEV运行，可以完全消除复杂性问题。
黑盒：黑盒模块意味着工具忽略其内部，其输出被视为模型其余部分的自由输入。黑匣子在FEV中更容易使用的一个关键区别是：在关键点映射阶段映射相应黑盒的输出，就像基本输入（primary input）一样；只要在两种设计中选择具有相应输出的黑盒，黑盒输出的必要假设是自动的，本质上假设两个模型中的相应输出相等。在FEV中，有几种明显的情况可以使用黑盒逻辑：

内存和缓存：内存和缓存是一些难以激活成功教程的难题，往往会导致FV工具的复杂性膨胀。如果正在使用包含内存和缓存的模型，通常使用黑盒最有意义。大多数存储器都会在晶体管级别检查RTL-netlist等价性。
可信IP：由第三方提供的、经过预先验证且用户的团队未接触的试块应该是安全的，可以忽略FEV。
已知的不变区块：如果正在验证设计更改，且知道设计的某些部分没有更改，那么使用黑盒。

层次型 FEV ：为了克服容量问题，FEV通常使用分层的方法进行处理。首先在一些较低级别的模块上证明FEV，然后在顶层证明这些子黑盒的等价性。例如，假设我们在验证图8.16中的设计时遇到了复杂性问题：

在图8.16中，有五个主要模块（A、B、C、D和E）以及与这些模块交互的周围控制逻辑。可以先验证两个模型中的块A是等效的，然后验证块B，依此类推。在分别验证了每个模块之后，就可以验证顶层模型，并将子模块黑盒化，做顶层FEV。为了实现这一点，需要约束综合工具以防止跨某些层次结构进行优化。

其他关键点（切入点）：默认情况下，组合FEV将主要输入/输出（primary inputs/outputs）和状态元素标识为关键点；序列 FEV通常只将输入/输出标识为关键点，如果一些内部状态元素也被识别为关键点，则可以执行得更好。切点是非状态点，被视为关键点，可以在两个模型之间映射和验证，就像组合FEV处理触发器和锁存器一样。确定关键切点可以大大减少需要验证的逻辑。但在某些情况下，通过隐藏证明下一个下游关键点所需的逻辑，添加选择不当的切点可能会导致误判，并产生更多调试工作。
分解案例：FPV环境中验证限制在某些模式或使用假设的情况下，可以显著降低复杂性。在多个FEV运行中，将模型限制为其功能的特定子集。
Don’t Care Assignments：这是FEV独有的问题。DC空间通常由RTL模糊性产生，较大的DC空间不仅会使验证问题复杂化，还会显著增加复杂性。因此，将包含DC空间的不明确RTL替换为每个操作都有明确结果的模型，有时可以显著降低FEV复杂性。FEV工具可能会提供直接修复DC空间的选项，例如，对于任何不明确的RTL分配，总是选择0。如果使用RTL–netlist FEV，在移除DC空间时需要使用相同的约束重新运行综合，否则可能会引入真正的不匹配。如果运行RTL-RTL FEV，需要小心地在两个模型中等效地移除DC空间。
禁用综合优化：在RTL-netlist FEV中，综合工具进行积极的优化会导致许多复杂性，这会明显重写组合逻辑锥。如果有一个FEV不收敛的模型，并且不能用上述任何其他方法解决它，用户可以告诉综合工具不要优化有问题的逻辑。大多数提供复杂优化的综合工具也提供了在模型的选定区域关闭它们的方法。

目前我也处在学习阶段，有错或者形容不准确的地方，欢迎大家指出！

今天的文章Formal equivalence verification 形式验证之等价验证 FEV 第8章分享到此就结束了，感谢您的阅读。

版权声明：本文内容由互联网用户自发贡献，该文观点仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容，请发送邮件至举报，一经查实，本站将立刻删除。
如需转载请保留出处：https://bianchenghao.cn/67310.html