Dinglei_hello · 2022年01月14日

搭建FPV验证环境

一、什么是FPV?

FPV是一种用来证明使用SVA或类似的语言描述的RTL属性的方法。

49face29565354692be3b87279d4f983.png

上图说明了一个FPV工具执行的框图。

FPV的输入:

  • 1、RTL模型
  • 2、要证明的一组属性:assertions 和cover
  • 3、一组约束条件:assumptions以及时钟、复位

FPV的输出

  • 1、已证明的属性列表(proven assertions)
  • 2、无法覆盖的场景(unreachable cover points)
  • 3、对于每一个被证伪的assertion 或可覆盖的cover point,展示一个波形示例
  • 4、FPV无法完全证明的属性列表(但是仍然有它的用处)。

FPV工具基于用户指定的输入约束,在数学上分析证明所有可能的逻辑空间都满足目标属性。不像EDA仿真,FPV不仅仅检查某些随机场景,而是检查所有合法的空间。

184c20d7c17fcfe8f0676d5446f4a25d.png

上图是一个FPV证明逻辑空间的示意,图中的每个像素点都是RTL设计中的状态(latches或者flops。

•紫色矩形表示RTL设计中的所有完整状态空间all possible RTL values
•设计的初始状态reset 状态reset states
•浅绿色的椭圆形代表了从reset状态起始可以覆盖到的状态(reachable states
• 橙色的椭圆形表示assumption ,排除了部分设计的逻辑空间。我们可以看到,Assume1和Assume3冗余地排除了部分unreachable 空间Assumptions
•深蓝色的矩形表示assertion ,定义了设计空间的某些子集为非法的,这是FPV的证明目标Assertions)。Assertion 1 pass了,因为所有的交集都被排除了(假pass);Assertion 2 pass了,同样因为和reachable states没有交集(假pass)。Assert3 fail了,因为它定义的一些非法状态是在reachable states。
•星星标记表示在当前FPV环境里覆盖点定义的状态集(Cover Points)。Cover1 可覆盖,因为它包含在reachable state内;Cover2无法覆盖,因为它的所有状态都被Assume2排除了;Cover3无法覆盖,因为它和reachable state没有交集

FPV这种基本技术在SOC研发流程中可以被用来:

•Design exercise FPV。利用形式验证的技术,不用创建testbench就可以探索设计的行为。
• Bug hunting FPV。针对一个使用EDA仿真验证的模块,验证其中的corner case。
• “Traditional” full proof FPV。针对一个复杂的设计,仅使用FPV 进行sign off,证明其满足所有的规格。
• Application-specific FPV。针对设计的某些特定功能,如控制寄存器、顶层连接、状态机和门控等等。

二、搭建FPV验证环境(一)—编译设计

为了更好地说明FPV的实际应用,本文首先基于一个密码锁的例子展示FPV验证的各个步骤。本文首先介绍RTL的编译,重点在后续文章。
2d5b98c448ec57d4ea55e384b4b24976.png

614b065f7de895d5ffa2b091456d6516.png

如上图所示,是一个简单的密码锁,密码锁需要连续输入一组3个特定的十进制数才能打开。这个密码锁的实现使用RTL编码。

module combination_lock ( 
input bit [9:0] digits [3:0], 
input bit override, 
input bit clk, rst, 
output bit open 
); 
bit [63:0] combo; 
decoder d1(clk, rst, digits, combo); 
combination_checker c1(clk, rst, combo, override, 
open); 
endmodule 

上面的设计中具有一个“override”接口,可以替代输入密钥组合。

基于这个示例仅仅是为了介绍FPV验证的流程,不考虑验证的完备性。所以暂定验证的目标为:

•在正确的输入组合{COMBO_FIRST_PART, COMBO_SECOND_PART,COMBO_THIRD_PART}下,锁正确地打开。
•在错误的输入组合下,锁不能打开。

基于这些目标我们才能开始我们的FPV验证,没有目标和计划去做的事情只能是不预则废。

除了目标和计划之外,编译设计之前还需要保证我们对设计的规格特别是接口非常了解,以及我们拿到的设计是可综合的RTL代码(在这一点上和EDA仿真验证有所区别)。

对于可综合的设计,也就是说不支持晶体管级的电路描述、行为级电路描述、面向对象建模等等。

如果你发现你的设计里面必须使用不可综合的硬件行为描述,那么你可能需要重新考虑下是否应该采用FPV这个验证手段了。

三、搭建FPV验证环境(二)

创建cover point

验证的最终目标就是证明,即证明RTL设计满足业务需求。Cover point就是这一切证明的前提,对于FPV更是这样,不然非常容易出现假 full prove。

很多执行EDA仿真的工程师常常将cover pont作为一个事后诸葛,这是一个严重的错误,没有依据基础的推理结果是站不住脚的。

在FPV工具中,cover point可以帮助确认验证环境是否发生过约,避免假PASS的出现。极端情况下,FPV工程师针对某个corener场景创建了数十个assertion,但是忽略了相应的coverpoint。在所有的assertion都被证明的情况下,该FPV工程师向验证经理报告这个模块已经全部验证完成了。结果在项目的后期才发现,由于使用了错误的约束assume,实际只验证了设计的极小一部分逻辑。

因此,我们建议在执行FPV是应该遵循下面这个关键的原则:

在开始执行FPV之前创建一组合适的cover point,包括你关注的一些corner场景。这些coverpoint就是FPV验证的立足点。

需要覆盖哪些场景是因设计而异的,依赖于设计的类型、业务场景以及验证工程师自己的关注点。常见的cover point包括:

•模块相关文档中的所有流程:将这些流程的波形翻译成SVA序列。
•输入输出的域段,以及必要的耦合场景(这个“必要”就要考验个人经验了)。
•状态机的每个状态。
•每个FIFO的空满状态。
•能够触发的异常类型。
等等。。。

对于前文我们提到的密码锁设计,可能没那么需要覆盖的coverpoint,但我们至少需要确保覆盖以下几个场景:

锁的开启和关闭。

c1: cover property (open == 0); 
c2: cover property (open == 1);

•输入的每个合法数字。

generate for (i = 0; i < 4; i++) begin 
  for (j = 0; j < 9; j++) begin 
    // We use a one-hot encoding 
    c3: cover property (digit[i][j] == 1); 
  end 
end 

我们不需要覆盖每一个数值,只需要利用等价原则覆盖典型场景值和一些特殊值。

创建assume

搭建FPV验证环境系列的第三篇文章是创建assume,即约束设计的输入行为。assume使FPV工具只专注于合法的场景,能够有效地降低验证证明的空间。关于assume,有一个关键的点只要注意:

  • 工程师并不能一开始就预想到所有复杂的场景,也永远不可能在执行FPV之前就想清楚并设置准确的assume。
  • 从添加一组简单的约束开始,而不是一开始就试图编写详尽无遗的约束。
  • 一开始新增的约束一般都是不足够的,还需在后续定位assertion时一步步新增assume,直到所有的assertion都PASS。

事实上,使用FPV工具进行验证的工程师大部分的时间都花在波形定位并新增assume的过程中。一开始只需要根据接口定义添加简单的assume约束。

在前文的密码锁例子中,我们有4个基于独热码的输入:

input bit [9:0] digits [3:0];

基于接口约束条件,我们只允许每个10比特中只有一个比特是高电平。

generate for (i = 0; i ,< 4; i++) begin 
a1: assume property ($onehot(digits[i])); 
end

当然,对于这个RTL设计可能还有其他更多的assume需要添加,我们可以在后续的debug中发现。

作者:验证哥布林
原文链接:
https://mp.weixin.qq.com/s/gayypz-hizOz5ZKyFN8W_g
https://mp.weixin.qq.com/s/1eo6w3mlW-_mRTtlFMbM0A
https://mp.weixin.qq.com/s/bBXRO_yXufKDj8s_5eiPZg
https://mp.weixin.qq.com/s/lAgDteOqedyb2kaNRAEV1w
微信公众号:
 title=

推荐阅读

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