formality: 形式验证流程

formality工具作用于设计开发过程中验证逻辑功能是否产生变化，不考虑layout与timing，可以作为动态仿真的替代品。受制于设计规模，仿真的时间与其输入向量的多寡有关，而formal verification不需要输入向量。

1.formality的使用场景

综合后: rtl网表与门级网表做对比，插入dft前后做对比。

后端设计后: 使用综合网表与后端布局布线后的网表做对比，eco前后做对比。

这里有两个概念，reference design和implement design，前者作为参考设计，后者作为修改过的设计。

2.formality验证流程

formality支持两种工作环境，formality shell和formality GUI。

2.1 formality GUI

1) Load Guidance

添加svf文件(记录综合优化过程的文件)，如果对比综合与后端网表，或者后端eco的网表的话一般不需要svf文件。

2) Load Design

读取reference design和implement design，以及相关的timing library文件，然后link。

read design file > verlog > load files

读取db文件，read DB libraries> DB > load files

设置top cell name并link design ，set top design > set top

添加implement design过程与reference design过程类似。

3) Performing Setup

读取设计后，需要设置formal verification环境。比如插入dft以后，做function验证时，不需要考虑scan mode/test mode(对应sdc中的set_case_analysis)，或者针对人为创建的port，需要给这些port设置一个常量告诉工具不去检查。另外使用tcl脚本去运行fm_shell的各种set_app_var都在"TCL Variables"中设置。

4) Matching Compare Points

检查 reference design 和 Implemention design 的比较点是否匹配：match>run matching

出现unmatched points也不都会导致verification失败，比如插antenna cell也会产生unmatched points，所以跑formality时候通常会跳过match这一步（看个人习惯）。

5) Verifing the Design and Interpreting Results

验证功能是否一致，verify> verify

出现"Verification succeeded!"就意味着成功了，如果有失败，就需要进行下一步，debug。

6) Debugging Verification

如果功能不一致，使用debug功能进行分析。

debug时会遇到一个logic cone的定义，logic cones是指从一个design object往回回溯，到另一个design object为止的中间所有的组合逻辑。

logic cones的起始点是formality中的compare point：

primary outputs, internal registers, black box input pins, or nets driven by multiple drivers where at least one driver is a port or blackbox。

logic cones的终止点是：

primary inputs or compare points。

2.2 formality shell

命令: fm_shell -f formality.tcl

set_app_var verification_clock_gate_hold_mode any

#允许implement design优化加入新的icg(高电平有效和低电平有效皆可)，如果设置set_app_var verification_clock_gate_edge_analysis true的话，set_app_var verification_clock_gate_hold any就失效了。

set_svf xx.svf

#综合过程文件，如果用插入dft之后的网表和原始网表对比就需要加svf文件。

set synopsys_auto_setup true

#会给undriven设成X属性，对于不检查的点可以设set_dont_verify_point {r: xx}比如某些pin的属性是inout，检查不过的情况。

read_db {

std.db \

mem.db \

…

}

read_sverilog -r $gloden_verilog

set_top r:/WORK/$top_cell_name

read_s verilog -r $imp_verilog

set_top i:/WORK/$top_cell_name

set_constant r: /WORK/top_cell_name/atpg_mode 0 -type port

set_constant i: /WORK/top_cell_name/atpg_mode 0 -type port

…

set_constant I:/WORK/top_cell_name/PEN_VDD_OPT 0 -type port

#这里给scanmode相关的port做了set_constant，因为scan的logic不做分析，还给一个opt的net做了set constant因为，这个net和对应的port是pr自己创建的，原始网表里没有，所以只在imp.v里设set_constant。

match

verify

analyze_points -failing