formality 中set_user_match的使用

似水如烟

在工程中，submodule通过formality的验证，打出matched的报告，注意以下描述：
1、通过fm_shell命令，以一条一条指令的方式执行脚本，让其停在matche之前，即只要执行了各种读入存在、环境设置类的操作，顶层及WORK也设置成功，此时，将原来打出的matched报告匹配的点使用set_user_match命令，指定这次验证的比对范围，却发生unknown name的错误（基本上都发生在多位寄存器），这种情况如何解决。
eg：上次操作打出的匹配报告：层次关系：counter/counter_cen.v------>lncid_reg[5:0]
Ref    DFF Name(Last) r:/WORK/counter/counter_cen_lncid_reg_0_
Impl  DFF Name(Last) i:/WORK/counter/counter_cen_lncid_reg_0_


在setup步骤，Ref：显示的格式为：Name(Last) r:/WORK/counter/counter_cen_lncid_reg[0]
Impl显示的和最终打出来的matched报告是一样的格式。


在使用set_user_match
r:/WORK/counter/counter_cen_lncid_reg_0_ i:/WORK/counter/counter_cen_lncid_reg_0_
和set_user_match
r:/WORK/counter/counter_cen_lncid_reg[0] i:/WORK/counter/counter_cen_lncid_reg_0_

均是错误的。

请问，哪位知道set_user_match正确的使用的。

似水如烟

找到问题原因了，写在这里，可能会有人遇到相同的问题。
出现上述问题是和综合过程有关的，当综合打散时，formality在解释RTL时，应该是根据svf文件只会保留cell/pin等的上一个层次，而更高的层次关系将全部被cut掉。

歪枣树

回复 2# 似水如烟


   请问楼主怎么解决的？利用DC产生了svf就能verify succeed?

似水如烟

这个和svf文件没有关系。如果综合采用打散的策略，网表没有层次，在formality读入时，将各design读入FMDatabase时，submodule的层次关系也是没有的（有可能会保留上一层，有可能是保留两三层），但matched报告的内容会打出所有层次的（这点也还没搞明白），在顶层使用set_user_match时，如果使用matched报告的结果，肯定就会出错。
采用了一种增量match的方法（自己想到的，不知对不对，但确实可用），先match一遍，然后使用set_user_match 吧matched报告内容source进去，之后，在match、verify。
我这种做法主要是在top-levle使用的，flatten。

keenforce001

不错不错

whzwwj1979

学习了

1027199631

回复 4# 似水如烟
大神，这个错误怎么解决啊？

1027199631

回复 4# 似水如烟


   
大神，这个问题如何解决啊？

1027199631

大神，这个问题如何解决啊？回复 1# 似水如烟

azkandf

Thanks for sharing!