搭建FPV验证环境（三）—创建assert
断言是整个FPV流程的焦点，即我们想要证明的最终目标。如果不考虑算力，理想情况下我们能够证明或者证伪所有的断言。
如前文所示，当我们在最开始搭建FPV环境时需要牢记:
第一次运行FPV时，查看cover比执行assertion证明重要得多。
想象一下下面这场景:你花了几个小时执行FPV，所有的assertion都PASS了。然而，你真的知道发生了什么吗?你如何说服验证经理和你自己，所有的corner case都得到了证明和保证？
事实上，很有可能你不小心对RTL过度约束了，从而有可能错误了corner case的bug发现。coverpoint能够证明当前FPV环境真正覆盖到了你关心的场景，可以增强验证的交付信心。
关于cover已经在前文提到过了，本文主要讨论同一个密码锁设计的一些断言assertion。
最关键的断言应该是正确的输入组合能打开锁，错误的组合不能打开锁，或者用逻辑学的语言，那就是“有且仅有特定的输入组合才能打开锁”。我们应该基于输入编写相应的端到端的assertion，检查输出:
sequence correct_combo_entered;
(digits == COMBO_FIRST_PART) ##1
(digits == COMBO_SECOND_PART) ##1
(digits == COMBO_THIRD_PART);
endsequence
open_good: assert property (correct_combo_entered | => open);我们还需要一个断言证明，当输入组合错误时（即3个输入中只要有一个错误）不能够打开锁。
相比断言一行复杂的表达式，更推荐书写多行简单的断言语句。
一般来说，debug简单的断言要比debug复杂的断言容易得多。
open_ok2: assert property (
open |-> $past(digits,3) == COMBO_FIRST_PART));
open_ok1: assert property (
open |-> $past(digits,2) == COMBO_SECOND_PART));
open_ok0: assert property (
open |-> $past(digits,1) == COMBO_THIRD_PART));不推荐下面这个写法：
open_ok_complex: assert property (open |->
($past(digits,3) == COMBO_FIRST_PART) &&
($past(digits,2) == COMBO_SECOND_PART) &&
($past(digits,1) == COMBO_THIRD_PART));上面的断言能够实现同样的功能，但是如果断言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. 使用
c2: cover property ((open == 1) && !$past(override));替换
c2: cover property (open == 1);2. 为了验证环境的目的，约束掉assume。
fix1: assume property (override == 0);根据我们的验证目标，override逻辑是比较边界的场景，可能藏有bug，需要在其他的断言中进行证明和覆盖，所以我们一般情况下应该使用方案1。但是，如果我们确定override在使用一直固定为高，则可以约束掉以简化FPV执行。
现在，让我们使用方案2，即加入这个assume并重新运行FPV，我们会得到c2的合理波形，如下图所示。
现在我们有了coverpoint波形，假设这个波形是合理，我们再开始debug我们的assertion。我们可以让FPV展示一个反例的波形，如下图所示。
在这个反例波形中，我们可以根据波形中的值来进行定位。fix完全部assertion或者RTL后重新执行FPV：
Done！一个简单的FPV执行完成了。
END
作者：验证哥布林
原文链接：
https://mp.weixin.qq.com/s/KoIURHDvSb2__Ifn7b-gvw
https://mp.weixin.qq.com/s/p7jrGn1Vb7sV9k2WaCjINQ
微信公众号：
推荐阅读
更多IC设计技术干货请关注IC设计技术专栏
