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

轻水一杯

问题1. FM跑到match指令的时候，图形界面显示match进度到26%，然后一直不动，好几天都不动，跑不下去。
问题2. 由于问题1，于是尝试跑工程中的一个module，也是比较多代码，但比问题1的代码少很多，于是跑下去了，结果很多unmatch信号，以及很多failing point, 查看后unmatch的点都是门口时钟信号的latch，编译用了-gate_clock 参数，但fm脚本也加了set verification_clock_gate_hold_mode any，以及DC对应的svf文件。查看failing point ，里面有几个信号是乘法器mathmul中的信号，于是修改脚本把比对的top module改成mathmul，fm结果成功。不解，为什么单独比对mathmul成功，而比对其上层module的时候，mathmul却比对失败。

望前辈高手赐教 ^_^

icfbicfb

fm在run的时候没必要开gui， 一般是run完 存了sesssion 后 start_gui 看比较结果，
开了-64bit 么，

svf加载了是吧， 总之rtl 比gate确实比较难，

yxu2006

可能是其他 和mathmul模块有连接关系的模块没有过。个人认为可以挑一些比较大的模块单独做fm。

icfbicfb

module怎么比formal，  set_top的名称不一样？

nicholas08

对formality不懂。如果是conformal到是可以帮你。。

submodule过了，顶层不过，那肯定是你submodule的某些input从顶层传过来时，不match...要自己去找。。
不过首先建议可以先设置所有的undriven signal to X..

轻水一杯

我尝试跑其中一个小模块，然后跟踪其中一个failing point ，逻辑锥比对的输入向量如图，从ref和imp的输入信号看，有两个信号不同，我查了DC的综合报告，

Information:In esign 'top', the register 'top_i/U_IMAGEA_DEC/U_QRDECODE/u_QRSearchBigBE/gb_pImgSrc_reg[4]' is removed because it is merged to 'top_i/U_IMAGEA_DEC/U_QRDECODE/u_QRSearchBigBE/gb_pImgSrc_reg[3]'. (OPT-1215)

gb_pImgSrc_reg[4]被merge到gb_pImgSrc_reg[3]，但是比对逻辑锥的时候，这个两个信号应该给相同的输入吧，但是从那个截图看，fm给是矢量是ref的gb_pImgSrc_reg[4]给1，而imp的gb_pImgSrc_reg[3]给0，这样比对，结果肯定是不对的。为什么fm没有认到那两个merge的信号。不知的我的理解是否正确，还是fm的时还有相关参数设置。

轻水一杯

问题1已经解决：改变了svf文件的产生方式。我原来的svf文件是 读入rtl代码 ，然后compile ，生成svf文件。后来修改为先读入rtl代码，产
                     生getch库的网表，然后输入getch库网表，compile 得svf文件。也就是svf记录的是getch 网表到compile后的网表的信息，
                     这样的svf拿去FM的时候，就不会卡在match了，而且verify出结果了，我FM的时候仍然是比对rtl和compile 网表。

新的问题：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？？？

轻水一杯

通过gui 的reference container  在work中可以找到MathDivDec1_1_40_0, 而svf中的名字是MathDivDec1_1_40，什么原因呢？

qioip

回复 7# 轻水一杯


   你好，我想问一下，如何让 DC  以getch库网标的形式输出，而不是目标库的？？谢谢

ocean_raft

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