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

ocean_raft

同问：
最后是如何解决到的呢？是因为读入RTL进入错误的吗？

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错误了吗？