一、什么是FPV？
FPV是一种用来证明使用SVA或类似的语言描述的RTL属性的方法。
上图说明了一个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不仅仅检查某些随机场景，而是检查所有合法的空间。
上图是一个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的编译，重点在后续文章。
如上图所示，是一个简单的密码锁，密码锁需要连续输入一组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
微信公众号：
推荐阅读
更多IC设计技术干货请关注IC设计技术专栏
