家»IC设计»基于正式的方法削减数字设计IP验证时间

基于正式的方法削减数字设计IP验证时间

文章：David Vincenzoni

更改执行验证的方法可以减少几周的验证时间。

当我们谈论数字IP的介绍时，我们指的是块的完整验证。设备数据表中列出的每个功能都需要验证。此外，每个寄存器传输语言（RTL）语句，BRANKE和表达也需要验证。只有当功能（功能“检查）和RTL代码覆盖范围达到100％时，IP才会签名。为了到达那里，我们可以考虑两种不同的模式来达到目标：通用验证方法（UVM）方法（古典方法）和基于形式的方法（新方法）。这是如何显着降低验证时间的方式。

古典方法论

多年来，我们已经使用UVM-SV / UVME方法来验证数字IPS。这种方法基于复杂的对象/方面取向语言，用于构建受机随机测试以验证数字块并发现错误。通过这种方法，我们可以通过简单地随机化数据生成来检查我们的块的功能并运行数百个测试，这有助于我们找到角落条件和/或死锁。

数字IP的验证环境的开发可以在以下任务中拆分：

UVM测试台开发（验证IPS，记分牌，跳棋）
UVM寄存器开发（验证配置和状态寄存器）
UVM测试开发（验证功能特征）
运行受限随机测试（UVM测试使用随机数据运行多次）
代码和功能覆盖提取
通过创建新测试和/或增加随机运行来改进覆盖范围

有时SystemVerilog断言（SVAS）在测试台中添加以检查特定条件，例如握手信号之间的关系。图1总结了这些步骤。

图1经典IP验证方法需要添加测试，直到达到足够的覆盖范围。

代码覆盖的步骤通常是在正式的不可发生流量的帮助下证实的。通过正式的无法接纳流量“改进”古典方法，使我们发现无法通过任何模拟涵盖无法涵盖的死/无法访问的RTL代码。以这种方式，从总体代码覆盖的计数中删除此类代码。

新方法

新方法基于正式验证流程。数字IP通过此方法完全验证和注销（正式签名）。该流程基于使用正式的应用程序和SVA代码的开发验证块的所有功能功能。至于基于UVM的流量，也可以将正式流分成多个任务：

RTL代码清洁用LINTING工具（RTL代码检查）
总线协议验证-e.g。高级微控制器总线架构（AMBA）总线 - 基于断言的验证IP（ABVIP）
控制和状态寄存器验证
正式财产验证（验证功能特征）
具有异步时钟域的IP的时钟域交叉验证（用于时钟和重置）
代码和功能覆盖提取
通过证明新的SVA断言来改进覆盖范围

图2.总结了这些测试。

图2.基于形式的验证方法是一种更精简的方法。

一旦RTL准备就绪，第一步是用正式的喷墨工具分析它。这可能导致Verilog / VHDL代码没有许多错误，例如：

死/无法访问的代码

经常，死亡/无法访问的代码可以隐藏一个错误。这是由正式的工具突出显示的，表明某些语句无法访问。设计师可以发现这种无法求的原因是代码中的错误

算术逻辑的数据溢出
巴士争论
有限状态机（FSM）死锁和现场锁定

这代表了FSM的首次验证

组合环
设计可测试性（DFT）检查

在扫描模式下完全控制时钟和复位

IP（例如AMBA总线）的总线协议可以通过ABVIP进行有效证明。该概念与UVM验证IP非常相似，主要差异是协议规则被遗忘验证。块的配置和状态寄存器可以轻松使用正式应用程序验证。可以检查任何类型的访问策略，不仅是简单的读/写或读数，还可以通过软件/读取软件或写入清除等。这个验证步骤是详尽无遗的。

对于Linting，总线协议和注册检查，设计人员无需编写任何SVA语句。正式的应用程序会自动生成断言以证明RTL代码。可以通过编写自定义SVA代码来验证IP的所有其他功能。正式的财产验证工具将详尽地证明断言。正式方法允许我们验证具有多个异步时钟的IPS的重新同步结构（例如握手）。在整个结构和正式分析中检查数据稳定性和重新同步触发器。

UVM流量，与正式流一样，可以提取RTL代码覆盖，以及功能覆盖。未达到覆盖目标时，开发并证明了更多的SVA断言。

UVM与正式

为了更好地了解UVM和正式的方法之间的比较，我们可以将RTL代码模拟在空间中的许多状态。

数字设计具有不仅与FSM相关的交易，而且还是数字协议总线和/或计数器的整体组合。这些州可以是数百或数千个，我们验证的范围是涵盖所有空间。

当我们使用动态约束随机测试模拟设计时，我们正在覆盖该状态空间的子集。图3.展示一个例子;黄色圆圈是可到达的状态空间，应验证和覆盖。通过UVM受限随机测试，绿圆是已经覆盖的状态空间。蓝色圆圈是不可达状态空间，其代表由于参数配置或非合法状态而代表死亡代码或无法访问的代码。