黑盒化技术简化FPV计算复杂性

黑盒的意思是说在FPV证明过程中忽略掉某些子模块以降低FPV的计算复杂性。

当一个模块被黑盒化时，它的输出被视为FPV设计的输入，即它们可以取任何随机值。部分模块的黑盒化对FPV的性能有着非常巨大的影响，所以在FPV证明的开始应该尽量地考虑任何黑盒化的可能。

黑盒化优化技术的一个好处是保证永远不会误报假pass（即本来应该fail,结果证明了所有的属性都proven了），因为黑盒化模块使其输出遍历了所有值，比实际设计能够覆盖的场景更多了。

当然，正因为黑盒化比实际设计的场景更多了，所有可能出现假fail，这个时候需要定位问题所在，然后非常慎重地增加相应的约束。

针对不同的FPV目的，很多常见的模块逻辑都应该被黑盒化。例如，memory的状态空间非常巨大，对于FPV工具来说很难全部覆盖而且数据的索引特性一般也不会是corner case，所以在某些不受影响的特性证明上是可以被黑盒化的。

一般来说，在计划运行 FPV 工具之前，可以考虑黑盒化下列几个模块：

memory和cache

复杂算法模块，例如乘法器、除法器、复杂函数或浮点逻辑

模拟电路

外部提供的（经过验证的）IP

审核编辑：刘清