Formality简介
Formality，synopsis的工具，我们常说的形式验证、formal check都是用它做的。作用就是比较两者“r、i”在功能上是否一致，跟时序一点儿关系都没有！
在数字ic的flow中，一般会做两次formal check： 一． rtl对DC netlist做一次；
二． DC netlist对PR后的netlist做一次。
先看个rtl对DC netlist的脚本：
#------------------------------------------------------------------------- # Formal check for Capture.vhd ( rtl vs dc_nlist ) #------------------------------------------------------------------------- set TOP_REF Capture set TOP_IMP Capture
set REF_NAME Capture.vhd set IMP_NAME Capture.v
set REF_PATH /home/project/9602-360-100/Dig/d1/work_jh/synop199/rtl
set IMP_PATH /home/project/9602-360-100/Dig/d1/work_jh/synop199/dc1/nlist set RPT /home/project/9602-360-100/Dig/d1/work_jh/synop199/fm/rpt
set hdlin_dwroot /edatools/synopsys/syn_vX-2008.9-SP4 set verification_failing_point_limit 2000 set synopsys_auto_setup true
set_svf /home/project/9602-360-100/Dig/d1/work_jh/synop199/dc1/default.svf
set search_path \
/edatools/synopsys/syn_vX-2008.9-SP4/libraries/syn\read_db {chrt35_ss_75_1pt3_SYNOPSYS2_MMSIM.db dw_foundation.sldb}
read_vhdl -r $REF_PATH/$REF_NAME -l work > $RPT/read_design.rpt set_top $TOP_REF > $RPT/set_top.rpt
report_hdlin_mismatch > $RPT/rpt_hdlin_mismatch.rpt
read_verilog -i $IMP_PATH/$IMP_NAME -l work >> $RPT/read_design.rpt set_top $TOP_IMP >> $RPT/set_top.rpt
#set_constant -type port r:/.../... 0 #set_constant -type port i:/.../... 0
match > $RPT/match.rpt
report_matched_points > $RPT/matched_point.rpt
report_unmatched_points > $RPT/unmatched_point.rpt
report_loops -limit 0 -unfold > $RPT/loops.rpt
verify
#以上内容可以放在一个文件里作为脚本，调用方法就是在fm_work下 $ fm_shell –f ../scripts/fm_rtl2dc.tcl
如果成功要看详细信息或者失败要debug的话，再输入start_gui，进入-GUI模式。
下面是DC netlist对PR netlist的formal check： #--------------------------------------------------------------- # Formal check for Capture.vhd （DC vs PR） #--------------------------------------------------------------- set TOP_REF Capture set TOP_IMP Capture set REF_NAME Capture.v
set IMP_NAME Capture_postlayout.v
set REF_PATH /home/project/9602-360-100/Dig/d1/work_jh/synop199/dc1/nlist set IMP_PATH /home/project/9602-360-100/Dig/d1/work_jh/synop199/astro set RPT /home/project/9602-360-100/Dig/d1/work_jh/synop199/fm/rpt_n2n
set hdlin_dwroot /edatools/synopsys/syn_vX-2008.9-SP4 set verification_failing_point_limit 2000 set synopsys_auto_setup true
#set_svf /home/engineer/gump/work_jh/capture/dc/default.svf
set search_path \
/edatools/synopsys/syn_vX-2008.9-SP4/libraries/syn\read_db {chrt35_ss_75_1pt3_SYNOPSYS2_MMSIM.db dw_foundation.sldb}
read_verilog -r $REF_PATH/$REF_NAME -l work > $RPT/read_design.rpt set_top $TOP_REF > $RPT/set_top.rpt
#report_hdlin_mismatch > $RPT/rpt_hdlin_mismatch.rpt
read_verilog -i $IMP_PATH/$IMP_NAME -l work >> $RPT/read_design.rpt set_top $TOP_IMP >> $RPT/set_top.rpt
#set_constant -type port r:/.../... 0 #set_constant -type port i:/.../... 0
match > $RPT/match.rpt
report_matched_points > $RPT/matched_point.rpt
report_unmatched_points > $RPT/unmatched_point.rpt
report_loops -limit 0 -unfold > $RPT/loops.rpt
verify
#以上内容可以放在一个文件里作为脚本，调用方法就是在fm_work下 $ fm_shell –f ../scripts/fm_dc2pr.tcl
如果成功要看详细信息或者失败要debug的话，再输入start_gui，进入-GUI模式。
建议fm工作结构：
../fm------- fm_run #formality工作目录
|------ reports #报告存放目录 |------ scripts #脚本存放目录