cut point可优化FEV的执行效率

电子说

1.3w人已加入

描述

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

cut point就是更细粒度的黑盒化。

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

模型

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

      审核编辑:彭静
打开APP阅读更多精彩内容
声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉

全部0条评论

快来发表一下你的评论吧 !

×
20
完善资料,
赚取积分