formality

刚开始接触formality，写了一个脚本用来匹配RTL代码和综合后的网表，出现的不匹配点非常多，不知道是自己写的脚本有问题还是综合的时候出现问题。想要哪位大侠提供一个正确的formality脚本，参考一下setup的设置。谢谢

同求啊

不太清楚

推荐用LEC

Fm.tcl
set VNET_LIST(r)/disk2/user/epon/epon/STA/back-anno/0530/top_0530.v
set VNET_LIST(i)/disk2/user/epon/epon/STA/back-anno/0601/ECO_0530_3_Route.vg
set TOPtop
set DATE[ sh date +%m%d%y ]
set SESSIONFM_${TOP}_${DATE}

sh rm -rf${SESSION}.run
sh mkdir -p ${SESSION}.run

source ./FM_setup.tcl
source ./slow_lib.tcl

read_verilog -container r -libname WORK $VNET_LIST(r)
set_top r:/WORK/${TOP}

read_verilog -container i -libname WORK $VNET_LIST(i)
set_top i:/WORK/${TOP}

match

report_unmatched_points > ${SESSION}.run/report_unmatched_points.rpt
report_matched_points> ${SESSION}.run/report_matched_points.rpt

set result [verify r:/WORK/${TOP} i:/WORK/${TOP}]

report_failing > ${SESSION}.run/report_failing.rpt
report_passing > ${SESSION}.run/report_passing.rpt
report_aborted > ${SESSION}.run/report_aborted.rpt

if { $result == 1 } {
exit
} else {
start_gui
}

Fm_setup.tcl
set sh_new_variable_message"false"; # default = "true"
set hdlin_auto_top"false"; # default = "false"
set hdlin_unresolved_modules"black_box"; # default = "error"
set verification_failing_point_limit999; # default = 20

slow_lib.tcl
set search_path {
/disk2/user/epon/epon/LIB/synopsys/SC
/disk2/user/epon/epon/LIB/synopsys/IO
/disk2/user/epon/epon/LIB/synopsys/MEM
}
foreach path $search_path {
foreach file [ glob -nocomplain $path/*.db ] {
if { ( [ regexp {_ss\.db$} $file ] == 1 ) || ( [ regexp {_worst\.db$} $file ] == 1 )} {
read_db $file
}
}
}
运行的时候，首先在fm.tcl中把文件名改好，
然后直接输入 fm_shell –f fm.tcl 就可以了。当然我们也可以把这三个文件合成一个文件，进行处理。

谢谢楼上的

谢谢！

多谢分享！
formal 无论是synopsys的 formality还是 cadence 的lec， 都很简单的，
就几步：
1）readlib/db
2) read reference netlist ( like RTL ) ,golden one
3) read implementation netlist , gate level , revised one
3) match , verify , lec mode
4) report results
但是formal里面最难就是rtl 比gate了，gate对gate很容易过，
比如综合后的和pr后的，上面这个脚本做gate对gate肯定够了，
你可以先比较下gate对gate，
RTL 对gate 要debug下，有的不是formal脚本的问题
对了，你读了 svf么，dc输出的 , 能帮助formal过的
set_svfdefault.svf

scanreorder以后，要把 test_mode ,test_se tie到0上， formal才能过
也就是忽略scanreorder对 scanchain 顺序造成的影响

report_unmatched_points有一堆不匹配的数据，但是report_failing的时候没有问题，是不是以后者为准

请教下，这个设置 set hdlin_unresolved_modules"black_box"; # default = "error"
是什么意思，有什么作用?还有就是关于黑盒一般有什么设置?谢谢了！

5楼活雷锋啊

一般自己就能匹配上。你可以试试naming first，修改下匹配规则

受教了

学习了

学习了、。、、

学习了，，顶

做等效性验证的，最关键一步就是。 mapping (LEC)/match(formality).把这个问题解决，后面大部分的问题都是工具的和设计的问题了

小编知道哪里下载formality吗?

Thank you.

遇到了这样的问题，等下试一下，谢谢啦

mark一下

不要忘了吃svf

五楼好人啊，谢谢