请教形式验证遇到的几个问题。
问题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却比对失败。
望前辈高手赐教 ^_^
fm在run的时候没必要开gui， 一般是run完 存了sesssion 后 start_gui 看比较结果，
开了-64bit 么，
svf加载了是吧， 总之rtl 比gate确实比较难，
可能是其他 和mathmul模块有连接关系的模块没有过。个人认为可以挑一些比较大的模块单独做fm。
module怎么比formal，set_top的名称不一样?
对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 referencedesign '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，什么原因呢?
你好，我想问一下，如何让 DC以getch库网标的形式输出，而不是目标库的?谢谢
同问：
最后是如何解决到的呢?是因为读入RTL进入错误的吗?
新的问题：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 referencedesign '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错误了吗?
formal永恒的恨啊
问题解决了没 虽然没有遇到此类问题，但很想学习下 望小编解决的话 能解释下！