ICC后的网表和DC后的网表进行形式验证时出现了一个问题[已解决]

ZHZIC

ICC后的网表是带VDD和VSS的，而综合后的网表是没有电源地的，这样的话我用Formality进行形式验证的话，第四步Match的时候，发现有170个点没有对上， ，看了一下，都是电源地没有对上， ，请问这个问题怎么解决啊，需要进行什么设置吗，还是不用管啊？

ZHZIC

感觉这个问题挺常见吧，毕竟PR之后多了电源地，奈何本人是新手，不知道怎么解决。。。

dummy_tony

写个不带PG的.v

ZHZIC

哦哦，谢谢您，就是pr之后生成一个不带pg的.v吗？
还有个问题，我的数字库里的verilog module文件只有一个不带pg的文件，那后仿的时候也用那个不带pg的.v文件吗？

optihack

ZHZIC 发表于 2020-8-9 18:32
哦哦，谢谢您，就是pr之后生成一个不带pg的.v吗？
还有个问题，我的数字库里的verilog module文件只有一个 ...

对， example 如下。 后仿不带pg

  #no pg, no physical only cells, and no supply statements
  write_verilog -exclude {scalar_wire_declarations leaf_module_declarations end_cap_cells well_tap_cells filler_cells pad_spacer_cells physical_only_cells cover_cells pg_netlist supply_statements} -hierarchy all $OUTPUTS_DIR/${DESIGN_NAME}.v

  #with pg, no physical_only cells, no diodes, and no supply statements
  write_verilog -exclude {scalar_wire_declarations leaf_module_declarations end_cap_cells well_tap_cells filler_cells pad_spacer_cells physical_only_cells cover_cells diode_cells supply_statements} -hierarchy all $OUTPUTS_DIR/${DESIGN_NAME}.pg.v

  #with pg, and with physical only cells
  write_verilog -exclude {scalar_wire_declarations leaf_module_declarations empty_modules} -hierarchy all $OUTPUTS_DIR/${DESIGN_NAME}.phy.v

ZHZIC

好的，多谢多谢

西顾

楼主您好！~ 请问icc后的网表和dc后的网表做形式验证的教程您有吗？可以麻烦分享一下嘛？

我没有找到教程，只有看到rtl和dc的教程，头疼哇！

或者您可以描述下有什么差别吗？我不知道应该读入哪些文件！
或者您的脚本可以分享一下我自己学习一下吗？

ZHZIC

西顾 发表于 2021-5-24 16:11
楼主您好！~ 请问icc后的网表和dc后的网表做形式验证的教程您有吗？可以麻烦分享一下嘛？

我没有找到教程 ...

rtl和dc后的验证是读vcerilog网表和dc后的网表
dc后的和icc后的验证是读dc的网表和icc的网表

西顾

ZHZIC 发表于 2021-5-24 16:23
rtl和dc后的验证是读vcerilog网表和dc后的网表
dc后的和icc后的验证是读dc的网表和icc的网表

谢谢楼主~感谢您的回复！！请问db文件和svf文件呢？ 我看我库里有很多db文件，不知道是不是要全读入？以及set _top -auto 他会找不到，我不知道是不是哪里操作有问题，可以看看楼主的脚本吗？我想根据脚本看看自己是哪里没做到 T T

西顾

楼主您好，如果有空的话麻烦看看，请问您是用icc写的不带pg的verilog文件吗？ 我用了五楼的方法不对呀！
分享了我写的脚本，verify也成功了。但是担心verilog没写全，所以想问问您生成不带pg的verilog的脚本是什么样子呢？