形式验证
形式验证是为了验证RTL代码与综合后的门级网表之间的逻辑等价性。功能是否等价，与时序无关。
形式验证在设计流程中的位置
- 在综合后：在综合的流程中通常会插入DFT，这样综合出的结果的逻辑关系可能会与RTL代码的等效逻辑不一致，因此利用利用形式验证来保证综合过程没有出错，逻辑正确。
- 后端布局布线后：使用综合网表和和布局布线后网表进行比较。
- 设计形式发生变化，则需要做形式验证。
形式验证的应用
- 综合的网表与RTL对比做形式验证。保证综合过程没有逻辑错误。保证综合后的网表正确。
- 后端网表与综合后的网表对比做形式验证。保证后端没有引入逻辑错误。
- 做ECO的时候，ECO后的网表与ECO后的RTL做形式验证。（ECO当芯片已经流片出去了，工厂只做了一个底层，但金属层还没做可以做metalECO，发现某些容易修的bug后可以利用一些冗余的cell改变某些连线来修掉这个Bug，修改后端网表的同时对RTL也进行相应修改，然后将这两个文件进行LEC比较）
formality验证流程
Guidance > Reference > Implementation > Setup > Match > Verify >Debug
gui界面启动
输入fm或者formality
0.Guidance
添加.svf文件，其为DC综合生成的文件，内含综合时的一些优化记录。
1. Reference
读入rtl设计文件，read design file > verlog > load files
设置DC工具路径：otpion>browse
读取db文件，read DB libraries> DB > load files
设置顶层文件：set top design > set top
2. Implememtation
读入网表文件，read design file > verlog > load files
设置顶层文件：set top design > set top
3.Setup
设置常量
4.Match
验证Reference和Implememtion的逻辑功能是否匹配
match>run matching
match completed
可以看到match和unmatch的points
5.Verify
验证rtl和门级网表功能是否相同
verify> verify
verification succeeded!
6.Debug
如果功能不一致，进行debug。
双击可以进去看到设计的原理图，进行对比debug。
end
最后跑完，打印出结果，可以看到Passing (equivalent)和Failing (not equivalent)，这里我们可以看出验证是一致的。
TCL脚本运行
//run_form文件
source run_form
代码语言：javascript复制fm_shell -file form_check.tcl //后台运行
#fm -gui -file form_check.tcl //gui界面运行
//form_check.tcl文件
代码语言：javascript复制set_svf -append {/home/IC/soc/form_test/svf/test.svf}
read_verilog -container r -libname WORK -05 { /home/IC/soc/form_test/rtl/verilog_test.v }
set hdlin_dwroot /opt/Synopsys/DC2015
read_db { /home/IC/soc/form_test/db/fast.db }
set_top r:/WORK/verilog_test
set_top r:/FAST/ACCSHCINX2
read_verilog -container i -libname WORK -05 { /home/IC/soc/form_test/netlist/netlist_test.v }
set_top i:/WORK/netlist_test
set_top i:/FAST/ACCSHCINX4
match
verify
