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的执行效率。
-
寄存器
+关注
关注
31文章
5390浏览量
121871 -
模型
+关注
关注
1文章
3412浏览量
49470
原文标题:FPV复杂度优化之cut point
文章出处:【微信号:芯片验证工程师,微信公众号:芯片验证工程师】欢迎添加关注!文章转载请注明出处。
发布评论请先 登录
相关推荐

新一代CUT75系列PCB基板式开关电源问世
常用优化编译选项对ARM平台的影响
SPC574K7x的CUT 2.3和CUT 2.4之间有什么区别?
Floating-Point设计编码风格与技巧
如何提高单片机程序执行效率

可以通过降低约束的复杂度来优化Formal的执行效率吗?
英特尔推出Hala Point全球最大仿神经形态系统,解决AI效率问题
怎么提升单片机代码执行效率
制造执行系统MES:提升企业生产管理的效率与优化生产过程

评论