形式验证

形式验证是为了验证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

fm_shell -file form_check.tcl  //后台运行
#fm -gui -file form_check.tcl //gui界面运行

//form_check.tcl文件

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