Dinglei_hello · 1月17日

搭建FPV验证环境(2)

搭建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工具会发生什么。我们的第一次运行收到的结果如下表所示。

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

FPV

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

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

f7930ac9b68cbf9ab6790204b1fb5864.png

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

282055cd6a9d7e1bbad10371c1aebb61.png

在上图中,我们可以看到在第二个周期中锁是如何被打开的,原因就是当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的合理波形,如下图所示。

94bc84e44e40a2515c6347a3bdc2a3cc.png

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

aec503474ac890069c1379ffcca45ee2.png

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

5cc2c02566d7323c483684c0645a22a9.png

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

END

作者:验证哥布林
原文链接:
https://mp.weixin.qq.com/s/KoIURHDvSb2__Ifn7b-gvw
https://mp.weixin.qq.com/s/p7jrGn1Vb7sV9k2WaCjINQ
微信公众号:
 title=

推荐阅读

更多IC设计技术干货请关注IC设计技术专栏
2 阅读 427
推荐阅读
0 条评论
关注数
8581
内容数
782
主要交流IC以及SoC设计流程相关的技术和知识
目录
极术微信服务号
关注极术微信号
实时接收点赞提醒和评论通知
安谋科技学堂公众号
关注安谋科技学堂
实时获取安谋科技及 Arm 教学资源
安谋科技招聘公众号
关注安谋科技招聘
实时获取安谋科技中国职位信息