请教形式验证遇到的几个问题。。。。。

ocean_raft

新的问题：verify的结果有一些failing point，都是除法器module里的寄存器。查输入patterns的时候，找原因如下
               比如svf文件中有guide_reg_constant \
                                           -design { MathDivDec1_1_40 } \
                                           { dividend_reg[40] } \
                                           { 0 }
             然后formality.log中有
                                 Info:  guide_reg_constant 4266 (Line: 42899) Cannot find reference  design 'MathDivDec1_1_40'.
                                 Info:  SVF Operation 4266 (Line: 42899) - reg_constant.  Status: rejected
              failing point 中 在input patterns中dividend_reg[40] 置1的时候 输出failing。

             我查reference 就是gtech网表，明明有'MathDivDec1_1_40'这个module，请教此问题要如何debug？？？


该问题我也遇到了，是读入RTL错误了吗？

orphan

formal永恒的恨啊

522526tl

回复 1# 轻水一杯

问题解决了没 虽然没有遇到此类问题，但很想学习下 望楼主解决的话 能解释下！

wxqy_anita

换一个更高版本的试试。

Yeong

我遇到寄存器的常值被优化了，读svf文件，这些reg_constant  rejected了，导致fail，这个要怎么解决呢