展示一个FPV执行空间的例子

1、展示一个FPV执行空间的例子

　　简单来讲，FPV是用来数学方法来证明，RTL符合用户指定的一堆property（一般是SVA书写）。FPV工具，基于输入的约束，用数学方法分析RTL逻辑执行的所有可能的空间。与Simulation不同，FPV会同时check当前约束所有合法的值。

　　FPV的输入一般有：

　　RTL

　　待证明的property：assertions， cover points

　　约束：assumptions， clock ， reset

　　FPV输出一般有：

　　证明了的property：proven assertion， unreachable cover points.

　　对于fail的assertion，或者reachable cover point

，都有一个对应的波形来显示failure或者reachbility

　　bounded or inconclusive proofs：不确定证明的一些assertion和coverpooint

原作者： 木马哥 验证工程师的自我修养