[经验]

搭建FPV验证环境之创建assert与执行FPV简析

罗星

2022-6-27 17:15:52

2638 FPV RTL

搭建FPV验证环境（三）—创建assert

断言是整个FPV流程的焦点，即我们想要证明的最终目标。如果不考虑算力，理想情况下我们能够证明或者证伪所有的断言。

如前文所示，当我们在最开始搭建FPV环境时需要牢记:

第一次运行FPV时，查看cover比执行assertion证明重要得多。

想象一下下面这场景:你花了几个小时执行FPV，所有的assertion都PASS了。然而，你真的知道发生了什么吗?你如何说服验证经理和你自己，所有的corner case都得到了证明和保证？

事实上，很有可能你不小心对RTL过度约束了，从而有可能错误了corner case的bug发现。coverpoint能够证明当前FPV环境真正覆盖到了你关心的场景，可以增强验证的交付信心。

关于cover已经在前文提到过了，本文主要讨论同一个密码锁设计的一些断言assertion。

最关键的断言应该是正确的输入组合能打开锁，错误的组合不能打开锁，或者用逻辑学的语言，那就是“有且仅有特定的输入组合才能打开锁”。我们应该基于输入编写相应的端到端的assertion，检查输出:

我们还需要一个断言证明，当输入组合错误时（即3个输入中只要有一个错误）不能够打开锁。

相比断言一行复杂的表达式，更推荐书写多行简单的断言语句。

一般来说，debug简单的断言要比debug复杂的断言容易得多。

不推荐下面这个写法：

上面的断言能够实现同样的功能，但是如果断言FAIL了，我们还需要进行2次定位以确定FAIL的根本原因。

搭建FPV验证环境（四）—执行FPV

现在所有FPV需要的元素已经在前面的文章依次介绍过了，我们可以开始真正执行FPV工具并查看一些结果。

FPV工具会根据我们的复位情况找出FPV执行的初始状态，然后分析从这个初始状态开始的所有逻辑空间。

FPV将尝试为每个cover point找到一个逻辑轨迹，并试图证明每一个断言。我们预期的结果是:

•对于每个cover point，展示一个可以查看波形的示例。如果失败，展示uncoverable状态。

•对于每一个失败的assertion，展示一个相应的反例波形。如果成功，则显示证明通过。

•不完全证明的assertion（bounded）。

让我们看看在一个密码锁实例上运行一个FPV工具会发生什么。我们的第一次运行收到的结果如下表所示。

初次执行FPV的用户第一反应可能会说:“我们的断言fail了;RTL肯定出了什么问题。”

FPV

你不应该着急将debug fail的断言作为第一步！我们应该先检查我们的cover point展示的一些预期波形行为是否合理。

Cover point c1是为了展示没有锁打开的情况。它的波形非常简单，刚从复位中出来，看到锁是未打开的，如下图所示。

Coverpoint c2展示了锁打开的情况。我们马上就能发现问题，因为我们的设计本来要花三个周期才能进入一个完整的输入组合，但是工具中看到的波形能在两个周期内打开锁，如下图所示：

在上图中，我们可以看到在第二个周期中锁是如何被打开的，原因就是当override为高时，任何时候都能打开锁。有两种方法可以解决这个问题:

1. 使用

替换

2. 为了验证环境的目的，约束掉assume。

根据我们的验证目标，override逻辑是比较边界的场景，可能藏有bug，需要在其他的断言中进行证明和覆盖，所以我们一般情况下应该使用方案1。但是，如果我们确定override在使用一直固定为高，则可以约束掉以简化FPV执行。

现在，让我们使用方案2，即加入这个assume并重新运行FPV，我们会得到c2的合理波形，如下图所示。

现在我们有了coverpoint波形，假设这个波形是合理，我们再开始debug我们的assertion。我们可以让FPV展示一个反例的波形，如下图所示

在这个反例波形中，我们可以根据波形中的值来进行定位。fix完全部assertion或者RTL后重新执行FPV：

Done！一个简单的FPV执行完成了。

原作者：验证哥布林