时序逻辑电路实验怎么做，时序逻辑等效性的RTL设计和验证流程介绍

很多朋友对时序逻辑电路实验怎么做，时序逻辑等效性的RTL设计和验证流程介绍不是很了解，六月小编刚好整理了这方面的知识，今天就来带大家一探究竟。

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

设计团队通常使用系统模型进行验证。就验证而言，系统模型比RTL具有优势，例如，系统模型易于开发并且具有优异的运行时性能。挑战在于如何在系统级验证和生成具有正确功能的RTL之间建立一座桥梁。一种叫做时序逻辑等价性检查的方法有能力在这两者之间架起一座桥梁，这种方法基于C/C或SystemC编写的规范来正式验证RTL实现。

本文将讨论商用图形处理芯片从系统级到RTL的设计和验证过程。在这个过程中，首先要开发系统模型，然后用它来确认文章指令的算术运算，再通过检查时序逻辑的等价性来验证RTL的实现。系统级过程

随着设计复杂度的增加，为了对整个系统进行仿真，系统级建模成为必然。随着功能划分、模块接口和软硬件协同设计，设计复杂度呈指数级增长，使得系统验证势在必行。目前常用C/C或SystemC进行系统级设计和验证。

本例使用C/C对文章处理算法模块进行建模。一旦系统模型得到调整和验证，RTL的设计人员就可以编写Verilog代码了。高级综合工具可以从系统代码生成RTL，但更常见的是工程师用RTL代码手动重写设计。是对设计的解释，而不是改造。尽管RTL的实现已经被各种验证测试平台所验证，但是通过基于仿真的方法来测试所有可能的状态是不可能的。

有许多验证工具和方法可以在设计过程中使用，包括基于断言的验证、随机激励生成和覆盖驱动的验证。上述方法可能在功能上是可靠的，但都不依赖于系统模型。时序逻辑的等价性检验方法可以直接将系统模型的这种置信度转化为RTL实现。

图形处理器市场在很大程度上受到图像质量、再现性能和用户购买机会的影响。对于负责开发最新图形处理器芯片的项目团队来说，上述因素要求他们快速开发新算法，拿出新设计。为了满足这一要求，可以使用系统模型来弥补初始规格和频带之间的差距。项目开始时，受控随机RTL模拟已经运行了几天，但验证工程师仍然担心会有“遗漏”的缺陷。

测试中的RTL可以实现文章和非文章指令，并使用在建项目的算术模块创建下一代文章处理芯片。

设计验证主要集中在21个文章指令上，从“并行转移”到“具有减少效果的绝对差异”。使用时序逻辑等价性检查方法的目的是借助C/C编写的原始系统模型，改进芯片级回归前的RTL验证，时序逻辑的等价性检查可以用来发现仿真中的遗漏缺陷，改进RTL设计的调试。

算法模块的系统模型由2391条C/C语句实现。这个项目的第一步包括改进C/C代码，以便时序逻辑等价检查器可以读取它。因为该模型最初不是为等价性检查而编写的，所以它的一些设计结构不符合顺序工具语言的子集。项目组用“”语句过滤掉没有明显硬件概念的结构，比如“重新解释强制转换”和“静态强制转换”。这些变化是通过修改C/C代码实现的。

以后在C/C开发过程中遵循编码指南后，就不需要修改设计模块了。

设计团队的下一个任务是设置验证环境。时序逻辑等价性检查需要在验证之前指定复位状态和时序差异，例如时序和接口差异。时序差异具体定义为I/O映射和设计延迟。对于用C/C编写的系统模型，可以添加一个瘦SystemC“包装器”来引入复位和时钟，而不改变C/C模型。

文章处理器算法块的RTL实现使用4559行RTL码，延迟是7个时钟周期。C/C系统模型的延迟是一个时钟周期，由SystemC“包装器”引入。然后，设计团队指定向每个设计发送一组新输入数据的频率。因为RTL是流水线结构，所以新数据是一个时钟周期接一个时钟周期输入的。这样，C/C和RTL的吞吐量为1。

时序逻辑等价性检查利用时序分析和数学形式化算法来验证这两种模型的所有输入组合是否总能得到相同的输出。与模拟不同，它并行验证所有输入条件。在这个项目中，相当于同时验证所有指令。因为每个文章指令实现一个特定的算法功能，所以设计团队可以决定一次验证一个文章指令，以提高调试效率。

知道被测指令比同时调试所有指令更容易识别与任何缺陷相关的逻辑。此外，当一次只验证一条指令时，时序逻辑等价检查器运行得更快，从而进一步提高了调试效率。

在验证第一个指令(VEC4ADD)时，在RTL模型中发现9个设计缺陷，在系统模型中发现1个缺陷。系统模型中发现的缺陷可以指导设计人员在以后的设计中如何消除C代码中的二义性。时序逻辑的等价性检查可以用10个或更少时钟周期的简化反例来确认设计差异。对于每个反例波形，生成的波形可以显示导致设计差异的确切输入序列。

图：因为RTL是一个流水线结构，所以新数据是一个时钟周期一个时钟周期输入的。因此，C/C和RTL有相同的吞吐量测试基准。对于每一条指令，时序逻辑等价法可以在5分钟内发现差异，并生成反例。时序逻辑的等价性检查也将以测试基准的形式生成反例，这些反例可以在仿真时与原始的C和RTL设计一起运行。测试基准包含一个监视器，因此它可以暴露在波形模式中显示的相同设计缺陷。

在这个项目中，反例基准被重用为单元级回归测试套件。在纠正了VEC4ADD指令代码中的问题后，时序逻辑等价检查器用52MB在361秒内验证了系统模型和RTL之间的等价关系。如果对指令进行穷举模拟，需要运行3.71034个测试向量，所以即使使用100万周期/秒的模拟器，也很难在我们的有生之年完成验证。

验证第一条指令（VEC4ADD）所需的全部工作历时4天，其中包括设置时间、对多个设计缺陷的调试及取得完全确认的时间。第二条指令利用与第一条指令相同的设置脚本，从而允许设计师立即投入调试。他们可以在两天内对第二条指令（VEC2ADD）的10个缺陷进行查找、纠错及纠错后的确认。通过推断，全部验证这21条指令需5到7周时间，实际用时取决于发现的缺陷数量。

当采用基于仿真的验证方法时，设计团队完成相同验证工作需要花6个月的时间。

验证结果

使用系统模型完成图形指令的RTL验证是成功的。总共发现了19个功能缺陷。借助简练的反例，时序逻辑等效性检查方法可以改进验证质量、缩短调试周期。找到的缺陷包括：不正确的符号扩展、遗漏的箝位逻辑以及初始化错误等，这些缺陷将导致图像质量的降低、软件设计反复或芯片返工。

时序逻辑等效性检查方法能够借助用C/C++或SystemC编写的系统模型发现缺陷和验证RTL实现。它无需额外的测试基准或断言就能提升功能验证效率。通过识别难以发现的缺陷以及那些被传统仿真方法遗漏的缺陷，时序逻辑等效性检查方法能把设计风险降至最小。

以上知识分享希望能够帮助到大家！