（一）FPV和Simulation的10个不同
基于前文，我们对于FPV工具已经有了基本的了解了，下面我们进一步分析FPV与EDA仿真（simulation）有何不同。
对于FPV和simulation差异以及各自应用场景的深刻理解能够以最大限度地提高我们的验证生产力。
- simulation工具
运行在特定的测试向量上，检查当前的值的行为与代码中每个assertions和assumptions的预期一致，并且确认是否覆盖了cover points。
- FPV工具
FPV工具分析了受assume限制的所有逻辑空间，这意味着它可以发现所有违反assertion的情况。
1 对于assertion
Simulation:报告当前测试用例是否违反了assertion;
FPV:报告是否存在场景违反了assertion，即作为FPV证明的目标;
2 对于assumption
Simulation:报告当前测试用力是否违反了assumption（同assertion）;
FPV:作为输入的约束，限制证明的逻辑空间;
3 对于cover point
Simulation:报告当前测试是否覆盖了特定场景;
FPV:报告FPV执行时是否覆盖了特定场景;
4 适合多大规模的设计？
Simulation:直到全芯片级，可验证可综合设计模型以及行为级模型;
FPV:模块级和子系统级，仅用于可综合模型;
5 如何覆盖特定的场景？
Simulation:基于逻辑执行路径，从输入下手（Describe the journey）;
FPV:基于目的地，FPV工具会帮你找到那条路（Describe the destination）;
6 检查什么值？
Simulation:基于输入激励，检查当前值;
FPV:基于所有可覆盖的空间，检查属性;
7 如何约束激励？
Simulation:主动约束，发送合理的激励，做加法;
FPV:被动约束，排除非法的场景即可。做减法;
8 如何约束内部信号？
Simulation:force，只会影响该信号的下游逻辑;
FPV:assume，会影响所有这个信号相关的逻辑;
9 何如debug问题？
Simulation:根据波形追信号;
FPV:根据FPV工具展示的反例波形定位;
10 追踪信号距离？
Simulation:根据设计可能需要成千上万个周期;
FPV:一般只有几十个周期;
（二）FPV能够运行多大的设计?
FPV和Simulation的第一个区别是：
Simulation几乎可以验证任何规模的RTL模型直到full chip（当然会存在仿真速度的考量）；而FPV只能够处理相对较小的RTL模型，通常针对模块级和子系统级的验证（大概几万状态空间以内）。
为什么FPV对设计容量有比较大的限制，很简单，针对相同规模的设计，FPV做的事情更多（更加powerful），FPV会分析RTL模型上所有可能的状态空间，而不仅仅是特定的激励场景。
简单来说，FPV就是对设计进行指数级的Simulation。所以，我们也不应该认为FPV无法处理大规模的RTL设计，这不是FPV难处理的本质原因。
1 仅关注设计的某些特性
针对大规模的设计，我们可以仅仅关注大规模设计中的某些特性部分，而不是对整个设计进行Full Prove。
2 优化掉无关的状态空间
另外，我们还可以使用许多FPV优化技术来降低RTL模型的复杂性。
（三）如何使用FPV查看设计的特定场景?
FPV和Simulation的一个主要区别是验证执行的方式区别，即我们应该给工具什么样的信息以完成我们的验证目标?更具体地说，对于我们的密码锁例子，我们如何能够查看到使锁打开的场景？
Simulation
在典型的simulation场景中，我们需要开发了一个用来激励设计的验证平台，决定发什么样的随机激励，然后检查输出和预期是否相符。在我们的密码锁示例中，如果你担心是否有错误的输入组合能够打开锁，你需要使用验证平台驱动给设计大量的随机值（包括时序上的组合）。如果你比较幸运的话，可能有希望发现这个bug。这个密码锁的单周期输入场景有10^4种，再组合3拍，共（10^4）*3种场景。
如果其中只有少数错误的组合值能够打开这个密码锁，而你的随机机制又没有对这种错误的输入组合（能够发现bug的组合）有概率偏向，就很难发现这个问题。即使我们有幸发现了一个bug（错误的输入组合能够打开锁），fix后还是不能保证是否还有另外的错误输入组合同样能够打开这个锁。
FPV
我们只是定义属性（property），然后询问工具，对于我们定义的合法场景中，这些属性是否总是正确的。
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));一旦定义了这些属性，FPV工具就可以尝试去证明所有的合法空间都满足，如果不满足就展示出反例供验证工程师定位。
最重要的，也是FPV的优势体现，一旦我们fix了所有FPV的反例，直到assertion PASS，就可以打包票说设计不存在错误的输入组合能够打开锁这样的bug。这是simulation做不到的事情。
（四）FPV是如何发送激励的
Simulation和FPV的一个区别是，激励方式的不同。
Simulation
在执行每次的测试用例时进行检查，即使我们运行了非常多的测试用例也只是检查了其中部分特定的、有限的值集合。当你查看测试用例波形时，总是需要询问 “我们是否覆盖了所有的输入激励?”
FPV
FPV检查所有可能值的集合，而不仅仅是特定的场景。如果在FPV上，我们能够证明密码锁RTL模型中错误的组合不能够打开锁，那么所有的状态空间都满足，不需要再检查某些其他的激励场景（因为已经得到了检查）。
但也有不利的一面:有可能因为assume的缘故未某些非法的场景排除掉，造成假fail，或者将某些合法排除掉造成设计状态空间过约，遗漏bug，造成假pass。
因此，
对于FPV验证，需要重点检视是否过约，是否假PASS；
对于Simulation，需要重点检视是否验得不够多。简而言之，
FPV激励是做减法，需要保证不会“多减”；
Simulation激励是做“加法”，需要保证不会“少加”。
END
作者：验证哥布林
原文链接：
https://mp.weixin.qq.com/s/b0Q36BCtn5QdGpo_SIYGbA
https://mp.weixin.qq.com/s/NElREw8KsTj8n9ryYQuXrg
https://mp.weixin.qq.com/s/JAmr4gg2UDnEM3o8Y50U7g
https://mp.weixin.qq.com/s/OW-evk3i_p1zvwwb-YQs2w
微信公众号：
推荐阅读
更多IC设计技术干货请关注IC设计技术专栏
