Formality的逻辑等价性检查介绍和参考脚本
专栏:iLoveIC March 13, 2024, 9:53 p.m. 325 阅读
本文整理了基本的formality流程和脚本

形式验证在芯片设计流程中的应用

形式验证是一种利用数学证明的电路正确性的验证方法学。具体来说分成两大应用。一种是SVA形式验证,检查电路是否与SVA规则一致。另一种是电路的一致性检查,检查RTL、网表之间的等价性。

image.png
应用一:SVA检查
image.png
应用二:LEC检查

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。

image.png
逻辑锥
image.png
Ref和Imp被拆分成逻辑锥分别进行检查

Formality可以用在数字设计流程的各个环节

比如,前端设计过程中RTL1 vs RTL2,综合后的RTL vs Syn Netlist,插入DFT后RTL vs DFT Netlist,布局布线后RTL vs APR Netlist。

在项目实践中,只要想对比两个设计或者网表是否一致,LEC技术都可以用。比如,做功能ECO之前通过LEC来确认修改的点。做Timing ECO后,确认是否有误影响到逻辑功能。

image.png
Formality在设计流程中的应用

formality的使用flow

image.png

参考脚本

下面是一个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的启动和运行

可以直接敲formality打开gui后,直接点菜单来操作,操作结束后formality会自动保存命令历史,稍加修改就可以保存成自己的脚本。也可以在gui的terminal窗口source脚本。

在项目中更常用的方式是,直接用fm_shell跑脚本。

fm_shell -f fm.tcl

参考文档

感谢阅读,更多文章点击这里:【专栏:iLoveIC】