时序逻辑等效性检查方法使设计风险降至最低

寄存器传输级(RTL)验证在数字硬件设计中仍是瓶颈。行业调研显示，功能验证占整个设计工作的70%。但即使把重点放在验证上面，仍有超过60%的设计出带需要返工。其主要原因是在功能验证过程中暴露出来的逻辑或功能瑕疵和缺陷等。显然，需要进一步改进验证技术。

设计团队一般采用系统模型进行验证。就验证来说，系统模型比RTL更具优势，比如系统模型易于开发且具有优异的运行时性能。挑战性在于如何在系统级验证和生成功能正确的RTL间建立起桥梁。一种称为时序逻辑等效性检查的方法具有桥接两者的能力，它是基于C/C++或SystemC编写的规范来对RTL实现进行形式验证。

本文将讨论商用图形处理芯片所采用的从系统级到RTL的设计和验证流程。在该流程中，先要开发出系统模型，然后用它来确认视频指令的算术运算，然后再采用时序逻辑等效性检查方法验证RTL实现。

系统级流程

随着设计复杂性的增加，为了仿真整个系统，系统级建模变得不可避免。伴随功能划分、模块接口和硬件/软件协同设计而来的设计复杂性呈指数形式增长，使得系统验证势在必行。目前常采用C/C++或SystemC进行系统级设计和验证。

本例采用了C/C++来建模视频处理算法模块。一旦系统模型完成了调整和验证，RTL设计师就可以编写Verilog代码。高层综合工具可以从系统代码生成RTL。但工程师更常见的做法是用RTL代码手工重新编写设计。它是设计的解释而非转换。即便已用多种验证测试平台对RTL实现进行了验证，采用基于仿真的方法也无法测试全部可能的状态。

在设计流程中有许多验证工具和方法可以采用，它们包括：基于断言的验证，随机激励生成和以覆盖率驱动的验证等。上述方法在功能上也许是值得依赖的，但它们都没有借助系统模型。时序逻辑等效性检查方法可以将系统模型的这种信心直接转换为RTL实现。

图形处理器市场受成像质量、再现性能和用户购买时机的影响很大。对负责研制最新图形处理器芯片的项目团队来说，上述因素要求他们迅速开发出新算法、拿出新设计。为了满足这种要求，可以采用系统模型来弥合初始规范和出带间的差距。当项目开始时，受控随机RTL仿真已运行好几天了，但验证工程师仍担心会有“遗漏”的缺陷。被测RTL设计可以实现视频和非视频指令，并用在建项目的算术模块来创建下一代视频处理芯片。

图1：C/C++系统模型中采用了SystemC封装器：不用改变C/C++模型就能引入复位和时钟信号。

设计验证

验证工作主要集中在21条视频指令，范围从“并行转移”到“具有缩小作用的绝对差”等操作。采用时序逻辑等效性检查方法的目标是借助用C/C++编写的原始系统模型在芯片级回归前改进RTL验证。时序逻辑等效性检查可以用来发现仿真遗漏的缺陷，并改进RTL设计的调试工作。

算法模块的系统模型是用2,391条C/C++语句实现的。该项目的第一步包含改进C/C++代码使得时序逻辑等效性检查器可读懂它。因该模型最初并非是为等效性检查编写的，所以其中的一些设计构造不符合时序工具语言子集。该项目团队使用“ ifdef >”语句，来滤析出没有明显硬件概念的构造，例如：“reinterpret cast”和“static cast”。通过修改C/C++代码来实现这些改变。今后，遵循C/C++开发过程中的编码指南后可以不再需要修改设计模块。

设计团队接下来的工作是设置验证环境。时序逻辑等效性检查需要在验证前对复位状态和诸如时序和接口差异等时序差异进行规定。时序差异被具体规定为I/O映射和设计延时。

针对用C/C++编写的系统模型，可以通过添加一个薄的SystemC“封装器”来引入复位和时钟，中间不用改变C/C++模型。

该视频处理器算法块的RTL实现用了4,559行RTL码，延时是7个时钟周期。C/C++系统模型的延时是1个时钟周期，它是由SystemC“封装器”引入的。设计团队随后规定一组新输入数据送至每个设计的频率。因为RTL是管线结构，因此新数据是逐个时钟周期输入的。这样，C/C++和RTL的吞吐量都是1。

时序逻辑等效性检查采用时序分析和数学形式算法来验证这两个模型的全部输入组合是否一直能得到相同的输出。与仿真不同，它并行地验证全部输入条件。在该项目中，相当于同时验证全部指令。因为每一条视频指令实现一个具体算法功能，设计团队可以决定一次验证一条视频指令来提升调试效率。

因为了解被测试的指令，所以与同时对全部指令进行调试相比，确认与任何缺陷相关的逻辑更加容易。另外，当一次只验证一条指令时，时序逻辑等效性检查器运行时运行得更快，从而进一步提升了调试效率。

当验证第一条指令(VEC4ADD)时，在RTL模型中发现了9个设计缺陷、在系统模型中找到1个缺陷。系统模型中发现的缺陷可以指导设计师如何在以后设计中消除C++代码中的歧义。

时序逻辑等效性检查能用10个或更少时钟周期的精简反例来确认设计差异。对每个反例波形来说，产生的波形可以显示导致设计差异的精确输入序列。

图2：由于RTL是管线结构，新数据是逐个时钟周期输入的。因此C/C++与RTL具体有相同的吞吐量。