formality验证中SVF读入

似水如烟

回复 9# henryshen2000

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

henryshen2000

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

wythelin

###########################################################
# 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
希望有所幫助

jamesjie

henryshen2000 发表于 2017-5-12 17:13
不用专门处理，在运行Formality读入SVF后，当前运行目录下会生成一个formality_svf目录，其中有转换的文本 ...

你好，rejected内容具体怎么debug，我这边目前显示有reference cell找不到，但是，网表里面真实有

skysand

bottom up

CZB的筱

bob_haohao 发表于 2013-9-27 16:06
你做的是FPGA的形式验证还是ASIC的形式验证，你可以使用一个tcl命令将你的SVF文件直接上成FM的运行脚本文件 ...

佬，我想问下为什么将这个选项设置为true后，就不报reg_constant和reg_merging了。是否会影响这个对比的判断