formality简介

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 #脚本存放目录