一文带你学会Formality

fomality是什么？

formality是S家的形式验证的工具，形式验证故名思意是完成一个表面逻辑的验证，通过导入rtl代码和DC综合后的门级网表，验证前后逻辑是否一致，是否DC将部分逻辑消除了。

使用步骤

0. 打开formality的gui界面

在终端输入formality即可打开GUI界面。

1. 导入svf文件

svf文件是DC综合过程中产生的文件，用来记录DC对网表产生的一些变化，防止后续的rtl和门级网表对应不上。

2. 读入verilog文件

上图为verilog文件添加界面。

在options中的variables的designware root directory中选择DC安装的路径。在VCS style options选项卡中的library file中选择应用的工艺库的.v文件，并add。

在set top design中选择顶层module进行set top，成功后ref上会出现绿色小勾。

读入rtl级代码过程中，有两点需要注意。

是否用到了IP，如果用到了IP，那么不需要在read design files中将verilog代码读入，而是在后续的read DB libraries中读入IP的db文件即可。

是否在design中直接用到了工艺库中的module，如果用到了需要在options中设置，具体如下图。

3. 读入网表文件

在impl栏中同样也是读入design 和 db ，只不过这里要读的是网表的design和db，和步骤二类似，如果调用了pdks的设计，也要在options中设置，而db读入过程中除了要读入IP的db，还要读入pdks的db。最后设置set top，成功后同样会出现绿色小勾。

4. setup

setup好像是为了带有扫描链和DFT的设计准备的，本人暂时还没用过

5. match and verify

全部设置完就可以mathc and verify了，如果通过的话会提示verify succeed。如果失败的话会具体提示哪些部分验证不上。比如

6. 注意事项

这里有一个很重要的点，DC 的set_svf一定要放在脚本最前面，否则有些改变不会记录下来，我就是因为这个原因有两个FF一直unmatch，还以为是latcg的问题，其实

set verification_clock_gate_edge_analysis true

这条语句可以将DC生成的latcg作用屏蔽。