Formality的逻辑等价性检查介绍和参考脚本

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

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

应用一：SVA检查

应用二：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。

逻辑锥

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

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

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

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

Formality在设计流程中的应用

formality的使用flow

参考脚本

下面是一个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跑脚本。