formality 形式验证时遇到的问题 请高手指点

在给rtl级和它综合出来的网表做formality时遇到困难，它不匹配和失败的点太多了，大约有上千个

verify 也有几百个错误

我给存储器设成了黑盒，但是还是不行，我打开图形化界面显示逻辑锥,查看后我发现reference中存储器的所有输入输出信号值全为1，而implementation中的全为0，然后我将它们强制置为相等，但是还是不行，错误更多了。

而寄存器的逻辑锥打开后：也是值不同，但是都是constant

到底是为什么会有上千个地方不行，为什么设为黑盒的地方还会说不行，

哪个高手能指点我一下啊，很急的··

大家是不是看不到图啊?太愁人了

是不是设置了constant，然后SCAN_MODE没有打开。

怎么样才能知道有没有插入扫描链呢?到底怎么disabled呢，我查不到哪个信号是scan怎么办呢?
进行诊断，查看其view logic cone 发现 r中的寄存器为0值，i中的寄存器为1值。而r中的存储器的端口值如d什么的为1，而i中的却为0，到底是为什么呢?
有哪位高手能解答一下啊?

mei ren zhi dao a

read_svf xxx.svf first！

有没有插chain ，这个可以看netlist

请问怎么设置打开SCAN呢

不懂，学习中...

你的design没有scan 模式的控制信号吗 ?

你综合时候直接做了dft，出来的网表已经是插链的?
如果是这样，那就要设置一些dft的管脚了，另外差没插链，看看网表中寄存器的si端是否连接，有连接就是插链，没插链的连接0
如果你只是综合的网表和rtl比对出现这种情况：
1.综合工具版本和formality版本是否匹配
2，是否读入了svf
3，确认rtl和网表版本是否一致
4，确认你读入了memory的库文件，没有读入仿真文件
5，确认你的memory是否需要设置user_match
因为rtl到综合的网表基本不需要设置什么东东，所以暂时想到这些，小编自己确认一下吧

不知道小编的问题解决了没有，如果解决了，能否讲讲插入扫描链后的网表要怎样才能和rtl code做formality?也请各位大侠发表一下各自的作法！谢谢！

谁有相关资料吗?