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

jnxu2007 · 发表于 2012-2-15 19:27:27

您需要登录才可以下载或查看，没有账号？注册

x

本帖最后由 jnxu2007 于 2012-2-16 18:36 编辑

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

verify 也有几百个错误

而verify失败的大都是寄存器和存储器的地方

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

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

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

还有就是怎么样才能知道有没有插入扫描链呢？到底怎么disabled呢，我查不到哪个信号是scan怎么办呢？
我连综合后的网表有没有插入扫描链都不知道

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

jnxu2007 · 发表于 2012-2-15 19:30:23

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

wxcarson · 发表于 2012-2-16 07:34:16

回复 2# jnxu2007

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

jnxu2007 · 发表于 2012-2-16 12:42:19

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

jnxu2007 · 发表于 2012-2-16 18:25:06

mei ren zhi dao a

A1985 · 发表于 2012-2-16 21:11:34

read_svf xxx.svf first!!

eagle654321 · 发表于 2012-2-23 18:07:54

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

strivenbu · 发表于 2012-3-6 15:55:18

请问怎么设置打开SCAN呢

maomao110007 · 发表于 2012-3-28 16:37:10

不懂，学习中...

williamliwei · 发表于 2012-3-28 20:33:37

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

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