Formality使用指南.docx

说明1

（一）图形用户界面进行形式验证1
design2
读取源文件3
设置搜索目录3
设置搜索目录4
加载源文件5
设置fifo为reference的顶层5
2brary),在Choose a design中选择顶层模块名fifo，点击Set Top按钮。此时在Implementation出现绿色的对号符。
(Setup)
在这一步主要是设置常量，比如对应一些增加了SCAN扫描链和JTAG链的设计，需要设置一些常量，使这些SCAN和JTAG等功能的禁止。 是源代码，只是综合的源代码，没有添加SCAN和JTAG链。故可以省略这一步
检查reference design 和 Implemention design的比较点是否匹配,点击Match按钮，选择Run Matching按钮，进行匹配检查。出现下图结果：没有不匹配的比较点，可以进入下一步。
点击OK键，完成。现在你已经准备好，可以进行和功能是否一致。
选择Verify按钮，点击Verify All，进行形式验证。
验证结束，结果出现“Verify”fail的对话框，提示两种功能不一致。
6. Debug
由于验证失败，系统直接进入DEBUG工作区。在Failing Points的报告工作区里显示两设计的出不一致的比较点,在Failing Points的报告工作区内点击鼠标右键，选择Show All Cone Size ,在Size栏里显示每个compar point所包含的cell的数目。一般调试是从cell数目最小的compare point
开始。在这里我们从第一个compare point开始。选择r:/WORK/fifo/push_logic/full_flag/q_out_reg[o], 击鼠标右键，选择菜单中的view Logic Cones，出现Logic Cones View窗口。
在这个新窗口里显示的是reference design 和Imeplemention design的原理图，观看这个原理图我们发现在Implementation的CLK网线是用红色标识的，在logic cone view中，用红色标识的net网线是表示错误的。我们观察发现在reference design的CLK中表示的logic值为0，而Imeplemention design的CLK中表示的logic值为1。为了找出CLK net值不同的原因，分别选择reference design和Imeplemention design的CLK网线，选择右键菜单里的Isolate Subcone命令，出现下图。
在图中可以看出在Imeplemention design
中驱动CLK的逻辑里多了一个反相器，这有可能是综合工具为了满足hold-time的要求而增加的反相器。我们可以修改网表文件和重新综合一个网表文件，来修改这个错误。在gate目录下有一个文件是修改后的网表文件。关闭Logic cone View,重新用作为Implementation design。选择Implementation，点击Read Design Files中的Verilog，点击yes来移除当前的Implementation Design设计（）。重新选择，点击Load files，加载文件。 Set top Design,选择WORK和fifo
同样，跳过Setup
点击Match,选择Run Matching，运行完后出现下图：
点击Verify，选择Verify all，运行完出现下图，提示“Verification Successded!”
点击OK后，出现下图，显示所有compare point都pass。
到此，完成形式验证。
7清理工作
选择工具栏中的remove reference 和remove Implementation按钮，移除reference design 和Implementation design
在formality的命令行输入：remove_library –all命令移除。
（二）命令行方式进行形式验证
在上一节不退出formality图形界面，在formality的命令栏中输入：history > ,生成脚本文件。退出formality图形界面
的内容
read_verilog -container r -libname WORK -vcs "-y /home/user/tutorial/rtl/ +libext+.v"
-0