在线咨询
eetop公众号 创芯大讲堂 创芯人才网
切换到宽版

EETOP 创芯网论坛 (原名:电子顶级开发网)

手机号码,快捷登录

手机号码,快捷登录

找回密码

  登录   注册  

快捷导航
搜帖子
查看: 10053|回复: 9

[求助] formality中出现unmatched points

[复制链接]
发表于 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?
 楼主| 发表于 2011-10-26 19:35:56 | 显示全部楼层
回复 2# 杀猪的日子


  是的
发表于 2011-11-14 16:11:46 | 显示全部楼层
坛子里玩形式验证的dx太少啊
发表于 2013-8-27 16:29:12 | 显示全部楼层
同样的问题呢,我也遇到了,求解,,,,
发表于 2013-8-27 16:31:46 | 显示全部楼层
RTL中有些触发器为固定状态,综合出来的网表会自动去掉这些触发器但是在做形式验证时,formality会提示这些触发器的地方为unmatched points
导致无法进行verify。
我现在不想去一一修改RLT中的触发器,在formality有没有什么选项或命令来解决这个呢?

不同的地方:

我已经set_svf ***.svf(dc之后的svf文件,在guidance时载入.svf文件)
发表于 2013-8-29 13:02:48 | 显示全部楼层
如果寄存器是固定的值的话,可以在setup阶段,把它设置为常数0或者1。图形界面可以操作的,不过回到setup后要重新match了。也可以在脚本中用命令,格式是:set_constant -type cell 寄存器名称 0;
发表于 2019-8-31 17:44:27 | 显示全部楼层
请问楼主有formality的详细一些的教程吗?现在有一个很简单的模块比对网表和RTL不一致,找不到具体原因是什么了,不知道是不是出现了你说的问题,还有就是那个DC生成的svf文件,是如何生成的,我综合完以后并没有找打这个文件啊
发表于 2019-8-31 17:48:48 | 显示全部楼层
ok,已经找到了,在Guidance中加载了svf文件,就可以比对成功了
发表于 2020-8-9 12:06:09 | 显示全部楼层
为什么我dc之后svf文件是空的啊,我也是有 固定状态的触发器
您需要登录后才可以回帖 登录 | 注册

本版积分规则

关闭

站长推荐 上一条 /2 下一条


小黑屋| 手机版| 关于我们| 联系我们| 在线咨询| 隐私声明| EETOP 创芯网
( 京ICP备:10050787号 京公网安备:11010502037710 )

GMT+8, 2024-11-26 06:40 , Processed in 0.049901 second(s), 8 queries , Gzip On, Redis On.

eetop公众号 创芯大讲堂 创芯人才网
快速回复 返回顶部 返回列表