formality中出现unmatched points

odielpx · 发表于 2011-10-25 23:22:53

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

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

x

RTL中有些触发器为固定状态，综合出来的网表会自动去掉这些触发器但是在做形式验证时，formality会提示这些触发器的地方为unmatched points
导致无法进行verify。
我现在不想去一一修改RLT中的触发器，在formality有没有什么选项或命令来解决这个呢？
我知道dc是可以在guidence载入.svf文件，但我是做的fpga设计的形式验证，好像并没有这个
.svf文件
多谢啊

杀猪的日子 · 发表于 2011-10-26 11:40:15

我不明白你在做什么比对？fpga综合netlist VS RTL code?

odielpx · 发表于 2011-10-26 19:35:56

回复 2# 杀猪的日子

是的

buhekele · 发表于 2011-11-14 16:11:46

坛子里玩形式验证的dx太少啊

zhqhzj · 发表于 2013-8-27 16:29:12

同样的问题呢，我也遇到了，求解，，，，

zhqhzj · 发表于 2013-8-27 16:31:46

RTL中有些触发器为固定状态，综合出来的网表会自动去掉这些触发器但是在做形式验证时，formality会提示这些触发器的地方为unmatched points
导致无法进行verify。
我现在不想去一一修改RLT中的触发器，在formality有没有什么选项或命令来解决这个呢？

不同的地方：

我已经set_svf ***.svf（dc之后的svf文件，在guidance时载入.svf文件）

0216liqian · 发表于 2013-8-29 13:02:48

如果寄存器是固定的值的话，可以在setup阶段，把它设置为常数0或者1。图形界面可以操作的，不过回到setup后要重新match了。也可以在脚本中用命令，格式是：set_constant -type cell 寄存器名称 0；

bysg312 · 发表于 2019-8-31 17:44:27

请问楼主有formality的详细一些的教程吗？现在有一个很简单的模块比对网表和RTL不一致，找不到具体原因是什么了，不知道是不是出现了你说的问题，还有就是那个DC生成的svf文件，是如何生成的，我综合完以后并没有找打这个文件啊

bysg312 · 发表于 2019-8-31 17:48:48

ok，已经找到了，在Guidance中加载了svf文件，就可以比对成功了

ZHZIC · 发表于 2020-8-9 12:06:09

为什么我dc之后svf文件是空的啊，我也是有固定状态的触发器

[求助] formality中出现unmatched points

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

相关帖子

站长推荐 /1