formality验证中SVF读入

hzdzkjly · 发表于 2013-9-26 09:39:36

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

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

x

综合采用的是bottom_up方式综合，而且各子模块单独做formality都是可以通过的，但是在做完顶层综合之后，对顶层做formality，却通不过。通过formality的debuge，发现问题都是formality在读入SVF文件时，有很多被formality给rejected了。这里想问一下坛子里有做bottom_up综合的朋友，你们在做形式验证时，formality读入SVF文件是怎么设置的。
很急啊，谢谢哪位好心的朋友给个提示。

bob_haohao · 发表于 2013-9-27 16:06:12

你做的是FPGA的形式验证还是ASIC的形式验证，你可以使用一个tcl命令将你的SVF文件直接上成FM的运行脚本文件试试，应该是FM的一些属性你没有设置对。你添加set synopsys_auto_setup true这条命令试试

hzdzkjly · 发表于 2013-9-28 09:52:09

回复 2# bob_haohao

我是做ASIC的形式验证。对于你说的set synopsys_auto_setup true 这个在我的脚本的开始处就已经设置了，而且底层综合的svf文件以及顶层综合的svf文件都用set_svf命令读进来，只是最后验证还是failed。由于svf文件里面有一些被rejected

hzdzkjly · 发表于 2013-9-29 11:19:52

自己再顶一个，别沉了呀，十足的技术贴，求高人啊

smartwang · 发表于 2013-10-9 10:54:59

fomality的版本和DC版本要对应，否则容易reject。

hzdzkjly · 发表于 2013-10-9 14:44:45

都是2012.06——sp5的版本，不是版本问题导致的。

A1985 · 发表于 2013-10-22 10:54:20

回复 6# hzdzkjly

fm版本高于DC半个版本是最好的！

henryshen2000 · 发表于 2013-11-14 15:19:04

现在我也遇到这个问题啊，SVF文件导入时很多reg_merging、reg_constant被Rejected了，导致最后verify很多Fail。也是不知道怎么解决啊。Formality的帮助文档也没有更详的说明了，难不成真的要试试DC的不同版本？

做个标记，解决了再来回复一下！

henryshen2000 · 发表于 2013-11-19 14:35:34

按bob_haohao说的，将svf中的命令转成FM的脚本执行，可以通过形式验证，但是总觉得手动介入较多不是很合适。

后来改用之前的DC版本综合出来的SVF也是可以直接通过FM形式验证的。

所以这样看来应该还是那里设置有问题，只能以后有空再来尝试了！

Haniel1986 · 发表于 2015-11-19 17:51:48

我都还没装上

[求助] formality验证中SVF读入

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

相关帖子

站长推荐 /1