formality验证问题

bysg312

1. 单独对一个小模块进行DC综合，然后使用formality对比RTL以及对应的netlist，是可以对比通过的
2. 增加一些其他的模块，上述的小模块不做任何改动(该小模块作为工程中的一个子模块)，经过DC综合以后，在使用formality对比RTL代码以及对应的netlsit，但是结果显示上述的那个原本可以验证通过的小模块中有三个信号比对不通过，

想问一下各位前辈，这个是什么问题？
因为单独对比那个小模块是可以通过的，说明应该没什么大问题，可是后续增加了其他的模块以后就不能通过了，这是什么原因导致的呢？

A1985

不通过的点 trace。罗脊椎是什么，。。。扥等

bysg312

A1985 发表于 2019-11-19 15:25
不通过的点 trace。罗脊椎是什么，。。。扥等

点开逻辑锥，显示不同的地方在于两个触发器上面，一个触发器的SD端是零，另外一个触发器的SD端是一，但是追溯到前面就会涉及特别多的电路了，感觉上是综合过程中做了哪些优化，导致触发器发生了变化

A1985

set dont touch...

jake

bysg312 发表于 2019-11-19 18:49
点开逻辑锥，显示不同的地方在于两个触发器上面，一个触发器的SD端是零，另外一个触发器的SD端是一，但是 ...

LEC 通常应该不比较 scan mode logic/scan path， 需要把 atpg_mode, scan_enable, scanin* 等都设置成 0， scanout 设置成 dont care/dont compare.  
如果已经有这样的设置，LEC 依然比较 SD pin, 说明 functional mode 和 scan mode 混在一起了， 有可能是设计本身的问题， 如缺了一个 scan mux 之类

bysg312

jake 发表于 2019-11-20 12:43
LEC 通常应该不比较 scan mode logic/scan path， 需要把 atpg_mode, scan_enable, scanin* 等都设置成 0 ...

为了避免SCAN带来的问题，我这一版的文件中没有SCAN，只是最原始的RTL代码(只有基本的IP功能，没有附加其他功能)，但是结果仍然无法通过

linibird

综合过程中出现了跨module boundary的优化。

bysg312

linibird 发表于 2020-1-5 11:55
综合过程中出现了跨module boundary的优化。

这个是什么意思？能麻烦给详细解释一下吗？

如果出现了这个问题，那应该怎么进一步解决呢？

还请大神指点一下，谢谢了

iamno11

带这种综合好的模块再综合的时候，一般会设dont touch，不然就会整体进行优化 导致你的子模块被改过了。
两种方法  1、按顺序吃两次的svf，一般可以过formal；2、综合的时候对子模块设dont touch

bysg312

iamno11 发表于 2020-1-8 11:28
带这种综合好的模块再综合的时候，一般会设dont touch，不然就会整体进行优化 导致你的子模块被改过了。
两 ...

好的，我按照您的建议试一试，谢谢了