用formality验证失败,怎样debug！！！

hopeman

    用formality做verilog网表dc_top.v和DC综合出来的门级网表dc_top.vg。用report_failing_points 报出所有匹配失败的点，其结果如下：


20 Failing compare points
( 20 matched , 0 unmatched ) ：
Ref
DFF
r:/WORK/dc_top/sys_top/conmax_top/m3/wb_ack_o_reg
Impl DFF
i:/WORK/dc_top/sys_top/conmax_top/m3/wb_ack_o_reg

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[0]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_0_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[10]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_10_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[11]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_11_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[12]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_12_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[13]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_13_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[14]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_14_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[15]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_15_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[16]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_16_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[17]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_17_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[18]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_18_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[19]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_19_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[1]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_1_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[20]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_20_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[21]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_21_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[22]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_22_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[23]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_23_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[24]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_24_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[25]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_25_

Ref
DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg[26]
Impl DFF
r:/ WORK/dc_top/sys_top/conmax_top/m3/wb_date_o_reg_26_

   我想知道，既然有20个DFF是matched，没有 unmatched 的地方，为什么还要报Failing compare ？？？
       我用start_gui 到图形界面，用命令
diagnose ，report_error_candidates 进行诊断，查看其view logic cone ，发现wb_ack_o_reg寄存器的数据端（D）在Ref和Impl中的值不一样，在Ref为0，在Impl中为1。
请问我该怎么debug，是修改门级网表dc_top.vg？？还是让前端工程师修改verilog网表dc_top.v，但是我不知道是什么原因让DC综合的时候产生这样的错误？？？我该如何在综合脚本里设置避免产生这种不匹配的错误呢？？？

ironszark

往前一级级的debug，直到找到问题在哪里为止。。

追天鹅的青蛙

好像学学formality啊，是不是代码增加新功能后可以用formality来验证其他功能是否受影响

kuangjianghua

综合一般不会出问题了，如果有的话，可能是三态总线出了问题，特别是存储器的输出端

yohuang

20 FF matched这里是指ref和Imp设计中有20个FF对应上了(mapped)，不是equivalent，一般来说综合出来的设计，没有插入DFT相关的东西是不会产生mismatch的，大都是你的setup有问题。不要随随便便去改dc_top.v, 有时候是因为register retiming还有phase inversion使得FF输入端是反向的，同时输出端也是反向的，这个在设计角度本身不是问题，所以你要可以设置允许register retiming,　其他的很多date_reg是不是有可能clk出问题了？怎么一个bus都出错了。楼上说的三态门也是一个考虑因素，你检查一下。另外，你看看你的matching Results summary table,看看是不是有unmatched　points.　你最好把ＤＣ综合的DC shell还有Formality shell给我们看一下，当然dc_top.v你要是方便的话也可以给我们看一下。

cchc1625

请问lz解决了么？ 我正好也碰到了这个错误了。。。
想请教解决方法

jnxu2007

回复 5# yohuang


    你好，看到你的解答感到你是fomality方面的高手，我也遇到楼主类似的问题，但是问题比他还多，有很多unmatched和很多failing的，有好几百，基本都是寄存器和存储器的，都是failing的点的值不一样，我把他们强制置为相等，可是又出现的别的问题，你能不能给我留个联系方式啊，我很急，真的非常感谢，我的邮箱xujinnainhit2007@126.com,请你帮帮我，我都纠结好几天了

jnxu2007

有没有高手知道这个问题呢，我现在也遇到了这个问题，r中的寄存器为0值，i中的寄存器为1值。而r中的存储器的端口值如d什么的为1，而i中的却为0，到底是为什么呢？

jnxu2007

i want to know```

mingxing00

遇到相同的问题了，输入时1，经过latch输出就变成0了~~
还有formality check遇见unmatch中类型为DFF0X，这是什么意思？感觉好像还导致verify失败