cut point可优化FEV的执行效率

cut point就是在模型中指定一个位置，将这个cutpoint的值设为随机值，去除这个点前后逻辑的关联性。 需要确认这个cut point的设定不会影响所需要证明的assert，如果影响了可以根据fail反例定位。 其实，这也类似于一个黑盒，只不过blackbox针对的是一个模块，将该模块所有的输出都设定为随机值，而cut point只是将特定的点（信号）设置为随机值。 一句话概括：

cutpoint就是更细粒度的黑盒化。

前面我们提到的FEV等价性验证中的每一个map点都是一个cut point。所以内部能够map上的点越多，FEV等价性证明的效率越高。 像黑盒化一样，cutpoint也是一个安全的复杂度优化手段，可能会导致假fail，但绝不会引入假pass。因为使用cut point后证明的空间比原来更大了，并且降低了被证明逻辑的复杂度。

在combinational FEV中，所有寄存器的状态都是一个cut point。在sequential FEV中，默认只会比较输出的一致性，如果添加内部某些寄存器状态作为map点，可以优化FEV的执行效率。

审核编辑：彭静