formality简介

更新时间:2024-02-03 19:43:01 阅读量: 教育文库 文档下载

说明:文章内容仅供预览,部分内容可能不全。下载后的文档,内容与下面显示的完全一致。下载之前请确认下面内容是否您想要的,是否完整无缺。

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

本文来源:https://www.bwwdw.com/article/sw5w.html

Top