如何对PR后网表进行形式验证

LQY2000

rt。

1. 首先关于Formality就不太明白。假如按照以下脚本执行

# Set var
set filelist "../ft/rtl_files.f";# file list name
set myFiles {}
for {set f [open $filelist r];} {[gets $f line]!=-1} {;} {
    lappend myFiles $line ;# get the names in filelist and turn into a list
}
close $f


set basename xxx;# change your top module name
set svfname ../sdc/result/${basename}.svf
set ntlname ../sdc/result/${basename}_netlist.v


#set hdlin_error_on_mismatch_message false


# Import svf
set synopsys_auto_setup true
set verification_clock_gate_hold_mode collapse_all_cg_cells
set_svf -append ${svfname}


###################
# RTL files
###################
# Import RTL verilog
read_verilog -container r -libname WORK -05 ${myFiles}


# Read RTL DesignWare


# Read db
read_db { /home/xxx/ICdigital616/180digital/svt/scx_csm_18ic_tt_1p8v_25c.db }


# Set RTL top
set_top r:/WORK/$basename


###################
# Implemented files
###################
# Import RTL verilog
read_verilog -container i -libname WORK -05 ${ntlname}


# Read RTL DesignWare


# Set RTL top
set_top i:/WORK/$basename


###################
# Run
###################
#Set current design
current_design $basename
# Run match
match
# Run verification
verify


# Report
report_status                         > ./report/${basename}_status.rpt


report_designs                        > ./report/${basename}_design.rpt
report_parameters $basename           > ./report/${basename}_param.rpt
report_multidriven_nets               > ./report/${basename}_multidriven.rpt
report_hierarchy  $basename           > ./report/${basename}_hier.rpt
report_analysis_results               > ./report/${basename}_analysis.rpt
report_failing_points                 > ./report/${basename}_fail.rpt


start_gui; # whether you like to enter GUI?
#exit; # whether you need to exit?

只要有set verification_clock_gate...这一句，那么Verify成功，否则必然不成功，也不清楚怎么样才是正确的。实际上应该不应该加这句话呢？


2. PR后网表验证
PR后（PR用的Innovus）网表验证时，需要导入SDC时输出的svf吗？只需要把网表文件从综合后的改成PR后的就可以吗？

zero_0

1. rtl vs. netlist:
对于综合工具插入的clock gating, RTL描述实际上控制的是数据，综合工具转成ICG会引入RTL中不存在的新的比较点，需要变量告诉formality按照 ICG的结构分析，要不就设 verification_clock_gate_hold_mode，更自动化的是设verification_clock_gate_edge_analysis

2. post-pr 网表验证：
一般综合后的netlist跟rtl比过后就可以作为golden的reference, 之后直接 pre-pr netlist vs. post-pr netlist 比过即可，一般没有用到综合引擎的话不用吃svf. 如果还要跟rtl比那当然要吃svf