形式验证是一种利用数学证明的电路正确性的验证方法学。具体来说分成两大应用。一种是SVA形式验证,检查电路是否与SVA规则一致。另一种是电路的一致性检查,检查RTL、网表之间的等价性。
应用一:SVA检查
应用二:LEC检查
在LEC检查前,读入的RTL和网表被分割成若干个逻辑锥。如下图,每个DFF和顶层Ouput Port是逻辑锥的终点。DFF的当前状态和Output Port值都可以用组合逻辑来描述。组合逻辑的输入可以是:顶层输入Port、前一级DFF的输出、BlackBox的输出等。
在做LEC时,RTL被称之为参考设计(Reference),Netlist称为实现电路(Implement)。Ref是标准,LEC检查就是检查Imp是否与Ref逻辑功能一致。
由于电路在综合、后端过程中会进行多轮时序、面积、功耗的优化,RTL中的DFF在Imp中不一定都可以直接找到,可能会被合并(reg merge)、复制(reg duplication)、打平(ungroup)、改名(change name)等。另外,在网表中还会插入门控时钟(icg)、测试电路(DFT)、低功耗单元(upf low power)。所以,做LEC检查最为关键的一步就是正确映射Ref和Imp中的DFF和Output Ports(keypoints)。大部分可以根据名字来自动映射,少数需要读入记录优化动作的svf文件,个别的需要手工设置来mapping。
逻辑锥
Ref和Imp被拆分成逻辑锥分别进行检查
比如,前端设计过程中RTL1 vs RTL2,综合后的RTL vs Syn Netlist,插入DFT后RTL vs DFT Netlist,布局布线后RTL vs APR Netlist。
在项目实践中,只要想对比两个设计或者网表是否一致,LEC技术都可以用。比如,做功能ECO之前通过LEC来确认修改的点。做Timing ECO后,确认是否有误影响到逻辑功能。
Formality在设计流程中的应用
下面是一个Formality参考脚本,可以根据自己项目的实际情况进行裁剪。
#------------------------------------------
# fm_shell -f this.tcl
#------------------------------------------
set verification_auto_session on
# user special setting in guide mode
guide
guide_reg_merging -design top \
-from u_a/u_b/c_reg \
-to u_a/u_b/c1_reg
# enter setup mode
setup
# set svf from syn
set_svf -append { $prj/syn/result/top.svf }
# set designware root path
set_app_var hdlin_dwroot { /eda/synopsys/designcompiler }
# read db
read_db {
$prj/lib/stdlib/rvt/frontend/synopsys/ss.db
$prj/lib/sram/sram1.db
$prj/lib/sram/sram2.db
}
# supress error to warn, for example:
set_mismatch_message_filter -warn FMR_VLOG-091
set_mismatch_message_filter -warn FMR_ELAB-147
# read rtl as reference, and set top design
read_verilog -r -05 -vcs "+define+AAA=1 +define+BBB" {
$prj/rtl/submodule1.v
$prj/rtl/submodule2.v
$prj/rtl/top.v
}
read_sverilog -r -12 {
$prj/rtl/algo1.sv
$prj/rtl/algo2.sv
}
set_top r:/WORK/top
# read netlist from syn as implement, and set top design
read_verilog -i -05 {
$prj/syn/result/top.gv
}
set_top i:/WORK/top
# set clock gating
set verification_clock_gate_edge_analysis true
# bypass dft, such as scan chain
set_constant -type port r:/WORK/top/test_mode 0
set_constant -type port i:/WORK/top/test_mode 0
set_constant -type port r:/WORK/top/scan_en 0
set_constant -type port i:/WORK/top/scan_en 0
set_dont_verify_points -type port r:/WORK/top/scan_out[3]
set_dont_verify_points -type port r:/WORK/top/scan_out[2]
set_dont_verify_points -type port r:/WORK/top/scan_out[1]
set_dont_verify_points -type port r:/WORK/top/scan_out[0]
set_dont_verify_points -type port i:/WORK/top/scan_out[3]
set_dont_verify_points -type port i:/WORK/top/scan_out[2]
set_dont_verify_points -type port i:/WORK/top/scan_out[1]
set_dont_verify_points -type port i:/WORK/top/scan_out[0]
# low power setting
load_upf -r top.upf
load_upf -i top_mapped.upf
# match and verify
match
verify
report_failing_points
# start_gui
# exit
可以直接敲formality
打开gui后,直接点菜单来操作,操作结束后formality会自动保存命令历史,稍加修改就可以保存成自己的脚本。也可以在gui的terminal窗口source脚本。
在项目中更常用的方式是,直接用fm_shell
跑脚本。
fm_shell -f fm.tcl