Formality形式验证教程

Formality形式验证主要验证综合后，生成的网表文件功能和之前的verilog文件功能是否一致，

需要两个文件，一个verilog文件，一个是网表文件

1.新建一个文件夹，把verilog文件和网表文件放入文件夹下，在此路径，打开linux下输入命令窗口，输入fm,则打开Formality软件

2. 切换到Ref界面下，导入verilog文件

3，设置路径，点击Options

4.  点击Browse，添加DC综合软件安装的根路径，如我的是/opt/Synopsys/Synplify2015/

5.点击VCS Style Options，然后在Library Directory（-y）下添加verilog的文件路径

 然后在Library Extension(+libext)下，写入verilog文件名，添加进去

然后加载

设置顶层文件

在ImpI.下添加网表文件，再加载

加入DB文件，文件在DC综合时添加库的路径下

 然后加载

设置顶层文件

然后，设置环境（Setup）

在这一步主要设置常量，比如对应一些增加了SCAN扫描链和JTAG链的设置，

由于fir.v是源代码，fir.vg只是综合的源代码，没有添加SACN和JTAG，故省略这一步

Match

Verify

Formality形式验证教程

原文：https://www.cnblogs.com/wojiaxiaoguo/p/10301635.html