formality验证中SVF读入

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

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

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

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

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

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

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

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

按bob_haohao说的，将svf中的命令转成FM的脚本执行，可以通过形式验证，但是总觉得手动介入较多不是很合适。
后来改用之前的DC版本综合出来的SVF也是可以直接通过FM形式验证的。
所以这样看来应该还是那里设置有问题，只能以后有空再来尝试了！

我都还没装上

hi，    你是如何将svf转成fm命令的?能说下方法吗
    谢了。

不用专门处理，在运行Formality读入SVF后，当前运行目录下会生成一个formality_svf目录，其中有转换的文本格式的命令，可以在Formality中运行。
另外，还可以用：report_svf_operation [find_svf_operation -status rejected] 命令报Rejected的内容。

###########################################################
# Synopsys Auto Setup Mode
set synopsys_auto_setup true
set_svf default.svf XXXX.svf
default.svf 是 DC default SVF file name. 一般document 都寫在DC中可以用set_svf 來改變檔名
但是在set_svf 這個指令之前的設定，都會寫在default.svf 內
所以在formality 中，必須讀兩個files
希望有所幫助