利用自动设置信息工具简化芯片设计等效检查

芯片设计过程中经常会对设计进行修改，因此需要对设计做等效检查，以保证设计的完整性。能传递设置信息的创建工具对于高效能检查非常重要，自动设置可使用户在验证出现问题时即刻加以解决，不会延长验证周期，并且不影响设计完整性。本文介绍利用自动设置信息工具简化设计之间的等效检查。

在芯片设计中，最后得到的结果常常因修改和优化而与原始设计有很大不同，那么如何对发生了重大变换的设计进行验证呢？如果验证工程师只有一点或根本不了解使用的优化工具与过程，则等效检查(EC)工具的设置就不能达到最优。而遗漏设置信息会影响到检验的等效性，同时也不能充分发挥验证的性能，设计实际上等效但却会得到一个不等效的结果(“虚假错误”)。即使验证工程师了解最优化过程，手工设置还是很费时间和容易产生错误，随着各种新颖设计问题也提出优化的要求，使得验证问题更加严重，这些问题对自动化方案很敏感，所以供应商们都在积极开发自动设置工具。

为了理解设计变换如何影响等效检查，我们必须首先了解等效检查流程中的一些基本要素。

等效检查是静态验证的一个分支，它使用形式与数学方法来证明一个设计的两种版本在功能上是否等价。等效检查流程由四个主要步骤组成，分别是读取、匹配、验证和调试。匹配和验证阶段受设计变换的影响最大。

◆读取：在读取阶段，两个版本设计都被读入等效检查工具，并分割成便于管理的分区，称为逻辑锥。逻辑锥是由寄存器、端口或黑盒围起来的一组逻辑，逻辑锥的输出边称为比较点。

◆匹配：在匹配阶段，等效检查工具将参考设计的比较点与最终设计中相应的比较点进行匹配或映射，可以使用非功能(基于名称)和基于功能两种匹配方法。为了使性能最佳，大多数匹配使用更有效的基于名称的方法来完成。

设计发生变换后会造成基于名称的技术只得到很少匹配逻辑锥，从而使匹配速度减慢。创建比较规则(指明各设计版本名称间关系的规则)有助于基于名称技术的使用，但规则本身的判定和创建也很费时间。当实现工具以随机方式生成名称时，设计规则就无法写出，比较点必须用手工进行匹配以得到最佳效果(图1)，或者用更昂贵的基于功能的技术来进行匹配，而这对于有很多不匹配点的设计却不实用。

◆验证：在验证阶段，每对匹配的比较点将被证明功能上是等价还是不等价。设计变换会影响逻辑锥的结构，当逻辑锥变化太大相差太远时，性能就会受到损害。在有些场合如重定时阶段，逻辑锥改变很大，以致需要进行附加设置才能成功完成设计验证。

◆调试：调试阶段从前一工具报告结果不等价开始。没有考虑到的设计变换会导致虚假错误结果，需要花费大量时间来调试实际上是等价的设计。通过调试分析，设计人员能够判定结果是否是由于一个未予解释的转换造成的，但好的方案应能在验证工具工作之前就先进行正确的设置。

创建设置脚本

因为在综合时经常会发生重命名和优化，所以上述验证过程对重大延迟或虚假错误很敏感。在等效检查完成后，用手工检查所有报告出的差异情况，找出那些由命名或重组问题所造成差异，然后为等效检查工具标出这些问题并再次运行，就可以纠正这些问题，但显然这不是最好的办法。

较好的方法是在那些会使等效检查产生问题的事件发生时就将其抓出来，并引导等效检查工具避免这些问题。这可以用手工来做，但要损失一些时间和精度，或者也可以用用户开发的指针工具对综合结果进行后处理，找出特定的名称或结构变换类型，但这不仅需要开发时间，且要对变换工具和等效检查工具能接受的自动指示有深入的理解，将无端浪费设计资源。理想情况下，工具供应商应使其工具自己提供变换信息，并编码成等效检查指示，使引导等效检查工具避免问题的全部过程能够自动进行，我们将这一过程称为自动设置。

执行设置文件

设置信息可通过各种执行工具创建，如综合、测试插入、布局与布线。对于等效检查，设置信息将包含必要的指令描述设计流程中发生的变换。例如当综合从设计中移走分层时，结果可能造成寄存器名称发生明显改变，RTL中的“Pre_bus_pipe_state_reg”会变成网表中的“r2345”这样一个不能直观看出来的转换。从综合过程中提取的设置信息将使验证工具把这些变化考虑进去，这样匹配的性能就与基于名称的技术相同。

再来看另外一个例子，即综合工具在寄存器间发生逻辑反相的情况。等效检查工具可以用手工设置来检测这种反相，但它可能需要调查每个寄存器以判断是否产生了移相而对性能产生影响。如果设置采用来自最优化工具的数据自动进行，将无需手工设置。此外，等效检查工具将仅仅调查认为可能有相位改变的寄存器，当相位改变能由工具独立证明时，整个设计可以非常有效地进行验证。

验证设计变换

这种方法能对跨工具应用的多种设计变换提供帮助，单对等效检查而言，它可以包括名称改变、常数寄存器删除、倒相、有限状态机重编码、合并冗余寄存器以及用于命名的先进算法应用。为说明这一过程，下面我们对三种具体转换进行详细说明，它们分别是名称改变、常数寄存器删除和冗余寄存器合并。

在综合过程中，寄存器名称经常会改变，如果基于名称的方法不能成功发现,则逻辑锥匹配将花费很多时间。直观的改变如把括弧变为下划线或者加一个_reg到名称中，这些都很容易用基于名称的方法来处理。但当名称有很大变动时，等效检查工具就得使用更昂贵的基于功能的技术。

名称改变与性能一起会影响设计验证的性能。为了完成验证，各版本设计之间的比较点必须正确匹配，如果有任何比较点改变使得对应锥不匹配，则没有附加用户设置的验证就不能够完成。

设置信息并不使用比较规则或者手工匹配来帮助基于名称的技术，但它提供一个机制传达这一信息，该方法具有很高的效率并保证所有设计中的比较点都完全匹配。

综合可能会去掉输出总是常数的寄存器，通常情况下常数寄存器会被一个常数1或常数0驱动器所替代。从纯功能观点看，因为附加逻辑不倒相，所以寄存器引脚总是保持数值1就可以用一个常数1所替代(图2)。

优化寄存器还可能使参考设计出现一些多余的寄存器，这些不会包含在最终的实现设计中。它可能带来两个问题，首先，在匹配时将有大量不匹配比较点信息需要用户检查，这很费时间，此外在过滤这些信息过程中，指明真正设计错误的不匹配点可能会被忽略掉；第二，验证过程中比较具有不同输入和逻辑设置的逻辑锥可能产生虚假错误。

如图3所示，最终实现锥的额外输入和逻辑使它在功能上不同于参考锥，因此要想成功验证取决于能否判定参考设计中寄存器c_reg是常数。

设置文件有助于解决这类问题。在匹配过程中，自动设置可以指示哪一个寄存器可能为常数，等效检查工具然后集中比较设计的其余比较点。考虑到匹配的目的，可以先假定设置信息正确，这一假设的有效性在验证中会进行确认。如果假设正确，验证将取得成功，当假设不正确时，比较点就不能正确匹配，于是得到验证结果不等价。

寄存器合并

寄存器合并是去掉一个或多个功能上冗余的寄存器。当寄存器具有相同的扇入和扇出时就认为是冗余的，当两个或更多信号经常为相同值时，冗余寄存器也会产生在RTL中。综合工具可以优化设计并且只使用一个信号寄存器，而不是为每个信号都用一个寄存器，寄存器的输出用来驱动原始寄存器的输出信号。这种最优化技术在门数特别重要的FPGA设计流程中普遍使用。

寄存器合并以后，RTL参考设计将含有多态保持寄存器(因而有多个比较点)，但最终实现设计(最优网表)只有一个比较点。如果没有额外的工具设置，逻辑锥就不能正确匹配，验证将得到虚假错误结果。另外也不能简单忽略掉额外的比较点，因为没有方法可以判断寄存器是否等价。

有些工具可以告诉如何寻找合并的寄存器，只需一步就可验证这类转换，然而在判断什么地方产生寄存器合并时需要进行搜索,所以会使验证变慢。

使用设置文件可以识别每次产生的寄存器合并，并作为设置信息传递给等效检查工具，检查工具就能知道到什么地方去寻找己合并的寄存器。证实寄存器在功能上是冗余的以后，等效检查工具就能执行合并，然后成功完成验证而不会对性能或设置产生不利影响。

使用这种设置文件具有明显的优点，但最终质量取决于能否从变换设计工具中得到正确信息，以及正确传递这些信息至等效检查工具的能力。为了使过程完全自动化，需要修改变换工具以得到数据，并修改等效检查工具，以接收自动设置文件。

作者：Osman Eralp

应用工程师

Synopsis公司