用等效性检查验证连续改变

为了满足对功率、性能和面积的要求，系统级芯片(SoC)和处理器设计团队面临着挑战。随着芯片复杂度的增加，设计团队必须验证成千行的代码以获得设计信心。为了取得成功，设计团队必须在紧迫的产品上市时间内达到系统目标和验证标准。

设计信心的增加是与独特测试序列的数量和系统级测试完整性呈函数关系。随着RTL修改的减少，功能验证投入增加，从而产生一种“已测试”模块。此时，仿真测试工具要花几天或几周时间完成，并且对设计改变非常敏感。功能验证中的确认要用数以亿计的仿真向量才能实现，难怪设计工程师临近设计末期都拒绝做出改变。

但是，如果最初的布局和布线结果显示设计不满足系统时序或功率目标怎么办？经过评估，设计工程师可能得出结论：通过对数据路径的检查，或许需要控制逻辑！这可能是一个简单的改变或一次重要的重写。恐惧之处在于重新验证经修改的设计需要多少工作，并且所做的改变让所有过去的功能验证投资付之东流水。

在这些境况下，大多数工程师主张做尽可能最少的侵入性改变。然而，这可能引起问题：在全局环境下简单修正在局部实现上变得复杂，或者使风险最小的修正可能不完全满足系统标准，且需要多次反复改变。对RTL的任何改变，无论有多小，都可能引入细微的负面影响。

连续改变(sequential change)

在大多数情况下，设计工程师通过把微架构转换到RTL代码来满足时序、功率和面积目标，微架构转换是连续的修改。当RTL模型经历优化时，设计工程师对关键设计功能如缓存大小、管线(pipeline)的数量和功率管理执行“what-if”分析。

在SoC和处理器设计中，功率、时序和面积特性难以评估和折衷。可供选择的微架构具有大量不同的数据路径，而控制逻辑的实现需要付出大量的工作进行开发和验证。

仿真可以被用于验证微架构优化。然而，仿真测试工具要运行数周，而连续的改变可能让现有的测试基准(testbench)失效。测试基准的效用因为设计延迟、吞吐量或I/O信号的差异性而降低。当发生这种情况时，测试基准需要手动检查和调整。

在许多情形下，测试基准比设计还要复杂，使测试基准的改变易受其自身缺陷的影响。根据情况，测试基准故障可能从模块级变化到子系统，或者甚至系统级测试。设计团队通过采用事务或握手接口写测试基准使连续改变的影响限制在局部。

图1：Averaged设计。

连续等效检查为设计工程师提供了另一种功能验证选项。通过证明具有连续差异的设计之间等效，所有早先的功能验证投入可以在未来RTL的实现中得到利用。连续等效检查确保微架构变换的功能正确性，给设计工程师以信心来进行设计后期的RTL改变。该技术也提供了对副作用的快速检测方法，并确保RTL优化与原始功能意图保持一致。

连续改变的实例

一个逻辑设计、模块或整个芯片可以看作由连续状态(或存储器)和组合逻辑构成的机器(machine)。组合逻辑负责计算下一个机器状态，该状态是任一时间点的输入和当前机器状态的函数。根据该逻辑是由moore机器还是由Mealy机器构成，机器输出是该时间点的当前状态和/或输入的函数。

图1中描绘的设计有四个输入值，它输出四个值的平均值及输入值3与平均值的绝对差。通过RTL代码、电路图和状态时序图完全描述了该设计。图1中Average4设计表示有一个状态级，即输出上的寄存器。

改变该设计以连续地读取输入数值就会修改状态和时序。这个连续变换是一个简单连续修正的例子。图2所示为Average4设计的连续输入实现，请注意到用于存储输入所加的寄存器、有限状态机(FSM)，以及相应的输出延迟。

在我们的例子中，图2中Average4设计在功能上等效于图1中的Average4设计。假设采用相同的输入序列，如果从一致的状态开始，经过一段时间两个设计都产生相同的输出，那么这一对设计被判定为等效。

在该例子中，简单的检查显示在图1周期N中的采样输出与在图2周期(N*4)+1中的输出匹配。这个例子证明，功能上等效的设计可能实质上存在组合逻辑及存储和访问状态方式上的差异。

连续变换以改善功率

随着芯片的日益复杂，需要在性能、面积和功率三者之间进行折中。随着设计从系统级向门级转移，对动态功率的影响逐渐减小。因此，改善动态功率的设计改变就是典型的连续改变，例如时钟选通和算子共享优化。

随着变化范围的增加，引入细微副作用的可能性增加。因此，要避免在设计过程后期做类似连续改变的重大修改，即使它们节省很大。这样可避免在向功率优化设计收敛的过程中产生严重的局限性，因为精确的功率估计需要布局和布线的电容信息。

下一个例子显示了用于改善功率的Average4控制逻辑中的连续改变。功率的降低通过利用共享资源和修改状态机编码以围绕单一加法器和寄存器迭代来实现。图3所示为经过功率优化的Average4设计。

功率管理开始于系统级，系统级模型运行要足够快以启动操作系统和运行应用跟踪(application trace)。这给出了开关行为的精确估计，系统级模型然后被优化为RTL实现。

RTL模型具有相同的功能，且可以考虑像电容这样的物理实现细节以进一步分析动态功率。有了功能精确的系统级模型就允许在系统级描述和RTL实现之间进行连续等效检查。

连续变换以改善时序

时序和长路径是常见的RTL设计问题。尽管改善时序的改变可能简单，可是设计过程后期的验证成本却相当高。

考虑一种改善时序的最小入侵性RTL改变，数据路径逻辑围绕管线触发器重定时序。这个连续改变解决了边际时序问题，并不大可能影响仿真测试基准。然而，传统的组合等效检查器无法处理重定时序逻辑，因为触发器不再被认为是等效的设计点。

在图4中，我们围绕在Average4设计中的状态单元对组合逻辑重定时序。为简化起见，在时序波形中的周期长度被缩短，并且在加法器、减法器、比较器和复用逻辑之间的详细寄存器布局从图中被省略。这些改变的最终增强了整个系统性能，而其功能与原始Average4设计相同。

当简单的重定时序达不到时序收敛时，需要做更大胆的连续改变。在此情况下，可能有必要增加管线级数。

重定时序RTL控制逻辑的特性造成一些非常难以验证的问题，经常引入边际缺陷(corner case bug)。例如，在CPU设计中，对管理指令级管线和多线程的控制逻辑进行连续重定时，会导致不仅难以调试而且难以仿真的活锁(live-lock)及其它错误。基于验证方法的仿真必须解决反应时间和吞吐量差异的问题，又要增加定向和随机测试来解决控制逻辑连续改变的问题。

图2：Averaged4电路的连续实现。

为了避免使测试工具重新生效来解决输出中的额外延迟，测试基准应该用反应时间可编程或反应迟钝的接口来写。设计工程师必须提前计划连续改变的验证，否则的话，这种日益增加的普通设计改变会对项目进度和成本造成负面影响。

连续等效检查

设计工程师快速处理连续改变验证的方法之一是利用连续等效检查器(sequential equivalency checker)。连续等效检查器验证新的RTL实现在功能上等效于早先已验证的参考设计，而不管状态、接口或连续微架构差异的变化。一个连续等效检查器可以在数分钟内检测出设计差异(如果存在的话)，立即向设计工程师提供关于RTL改变的反馈。不依赖于测试基准或工具，连续等效检查利用一个用Verilog、VHDL、SystemC或C/C++写成的RTL黄金模型或系统级参考设计。与组合等效检查器不同，连续检查器证明跨连续级和数据抽象的功能等效性。像重定时序和资源共享这样的连续改变仅需要较小的变化来设置参数以反映新的时序信息。

本文小结

对功率、时序和面积的微架构优化经常会导致RTL数据路径和控制逻辑的连续改变。连续改变对功能验证有相当大的影响。它们不仅需要对整个设计进行仔细的重新验证，而且它们还会令仿真测试基准失效。设计团队发现他们本身已陷入完成系统级要求、最小化设计改变和功能验证完整性的重围之中。

在设计过程后期的连续改变会日益频繁，设计工程师应该通过压缩测试基准接口并利用连续等效检查来改善其功能验证。连续等效检查不用测试基准就可以验证设计、快速识别设计负面影响，并自然地用连续差异处理设计。

最后，能够满怀信心地做出和验证连续改变，会大大地提高设计工程师在做系统优化时的工作效率，并使设计团队能够满足其迫切的功率、时序和面积目标。

作者:Mitch Dale

产品市场总监

Duncan MacKay

方法学顾问

Venkat Krishnaswami

工程总监

Calypto Design Systems公司