Formality使用指南.ppt

《Formality使用指南.ppt》由会员分享，可在线阅读，更多相关《Formality使用指南.ppt（63页珍藏版）》请在课桌文档上搜索。

1、Formality使用指南,检查RTL与GATE网表检查GATE网表和插入扫描链的GATE网表检查带有扫描链和JTAG链的GATE网表和插入扫描链的GATE网表,提 纲,说 明,FiFo的Tutorial目录下包含以下几个子目录：Rtl：fifo的RTL源代码；包含fifo.v,gray_counter.v,push_ctrl.v,gray2bin.v,pop_ctrl.v,rs_flop.v。Lib：门级网表需要的技术库；包含lsi_10k.db。Gate：综合的门级网表；包含fifo.vg 和fifo_mod.vg。Gate_with_scan：插入扫描链的门级网表；包含fifo_with

2、_scan.v。Gate_with_scan_jtag：带有扫描链和JTAG链的门级网表；包含fifo_with_scan_jtag.v。,一.检查RTL与GATE网表,RTL源代码：fifo.v门级网表：fifo.vg检查文件fifo.v和门级网表fifo.vg的功能一致性设置RTL源代码fifo.v为reference design设置门级网表fifo.vg为Implementation design,（一）图形用户界面进行形式验证,在UNXI提示符下进入tutorial目录：输入fm（或formality）。,1.设置reference design,点击formality图形界面的re

3、ference按钮，进入Read Design File点击Verilog按钮，出现添加Verilog文件的对话框。如下图：,1.1读取源文件,在对话框中选择：Rtl目录下的fifo.v文件，点击Open按钮,打开fifo.v源代码。如图：,1.2设置搜索目录,点击option按钮，出现set verilog read option对话框,选择Variable,在DesingWare root directory(hdlin_dwroot)出输入：echo$SYNOPSYS 或Design Compiler的安装目录(本工作站的目录为/opt/tools/synopsys)，如下图：,1.3设

4、置搜索目录,在Set verilog read option对话框中的VCS Style Option中选择Library Directory(-y),在Enter Diectory Name处浏览选择rtl目录然后点击add按钮添加查找目录rtl。,选择Library Extension(-libext)，在Enter File Extension处填上后缀名.v，然后点击add按钮添加，点击OK按钮。,1.4加载源文件,然后点击LOAD FILES按钮，加载源文件fifo.v，如下图：,1.5设置fifo为reference的顶层,在点击Set Top Design按钮，出现下图。,在ch

5、oose a library 中选择WORK，在choose a design中选择fifo（顶层设计的模块名）在Set and link the top design中点击Set Top，出现下图同时在Reference按钮上出现绿色的对号符：,2.设置Implementation Design,点击Implement按钮，在Read Design Files 中点击Verilog，出现Add verilog files对话框，选择gate目录下的verlog网表文件fifo.vg，点击Load Files加载网表文件fifo.vg，,2.1加载Technology library,选择Re

6、ad DB Libraries按钮，点击DB按钮，出现Add DB Files对话框选择lib目录下的lsi_10k.db库文件，（确保Read as share library被选中）点击LOAD Files，加载库文件。,选择Set Top Design,在Choose a library中选择WORK(Design Library),在Choose a design中选择顶层模块名fifo，点击Set Top按钮。此时在Implementation出现绿色的对号符。,3.设置环境(Setup),在这一步主要是设置常量，比如对应一些增加了SCAN扫描链和JTAG链的设计，需要设置一些常量，

7、使这些SCAN和JTAG等功能的禁止。由于fifo.v 是源代码，fifo.vg只是综合的源代码，没有添加SCAN和JTAG链。故可以省略这一步,4.Match,检查reference design 和 Implemention design的比较点是否匹配点击Match按钮，选择Run Matching按钮，进行匹配检查。出现下图结果：没有不匹配的比较点，可以进入下一步。,5.Verify,点击OK键，完成。现在你已经准备好，可以进行fifo.v和fifo.vg功能是否一致。选择Verify按钮，点击Verify All，进行形式验证。验证结束，结果出现“Verify”fail的对话框，提示

8、两种功能不一致。,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_rego,击鼠标右键，选择菜单中的view Logic Cones，出现Logic C

9、ones 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

10、 Subcone命令，出现下图。,在图中可以看出在Imeplemention design中驱动CLK的逻辑里多了一个反相器，这有可能是综合工具为了满足hold-time的要求而增加的反相器。我们可以修改fifo.vg网表文件和重新综合一个网表文件，来修改这个错误。在gate目录下有一个fifo_mod.vg文件是修改后的网表文件。关闭Logic cone View,重新用fifo_mod.vg作为Implementation design。选择Implementation，点击Read Design Files中的Verilog，点击yes来移除当前的Implementation Desig

11、n设计（fifo.vg）。重新选择fifo_mod.vg，点击Load files，加载文件。Set top Design,选择WORK和fifo,同样，跳过Setup点击Match,选择Run Matching，运行完后出现下图：,点击Verify，选择Verify all，运行完出现下图，提示“Verification Successded!”,点击OK后，出现下图，显示所有compare point都pass。到此，完成形式验证。,清理工作,选择工具栏中的remove reference 和remove Implementation按钮，移除reference design 和Imple

12、mentation design在formality的命令行输入：remove_library all命令移除technology library:lsi_10k.db。,（二）命令行方式进行形式验证,在上一节不退出formality图形界面，在formality的命令栏中输入：history fifo_rtl_gate.fms,生成脚本文件fifo_rtl_gate.fms退出formality图形界面,fifo_rtl_gate.fms的内容,set hdlin_dwroot/opt/tools/synopsys_2003.06 read_verilog-container r-libna

13、me WORK-vcs-y/home/user/tutorial/rtl/+libext+.v-01/home/user/tutorial/rtl/fifo.v set_top r:/WORK/fiforead_verilog-container i-libname WORK-01/home/user/tutorial/gate/fifo_mod.vg read_db-container i/home/user/tutorial/lib/lsi_10k.db set_top i:/WORK/fifomatchverify,命令行方式运行,在unix命令提示行下输入命令：fm_shell f f

14、ifo_rtl_gate.fms unix命令提示行输入命令fm_shell，进入formality的命令行模式。在formality的命令行模式fm_shell提示符下输入命令：source fifo_rtl_gate.fms,检查RTL与GATE网表检查GATE网表和插入扫描链的GATE网表检查带有扫描链和JTAG链的GATE网表和插入扫描链的GATE网表,提 纲,二.检查fifo_mod.vg和 fifo_with_scan.v的功能,设置fifo_mod.vg为reference design设置fifo_with_scan.v为implementation design,1.set

15、referenc design,点击reference按钮，在Read Design Files 中点击Verilog，选择gate目录下的verlog网表文件fifo_mod.vg，点击Load Files加载网表文件fifo_mod.vg在Read DB Files 中点击DB加载lsi_10k.db库文件，点击Load Files加载Set top，设置fifo模块为顶层。,2.set implementation design,点击implementation按钮，在Read Design Files 中点击Verilog，选择gate_with_scan目录下的verlog网表文件f

16、ifo_with_scan.v，点击Load Files加载网表文件fifo_with_scan.v可以省略Read DB Libraries这一步，因为在设置fifo_mod.vg时，我们已经加载lsi_10k.db为共享库文件。Set top，设置fifo模块为顶层。,3.setup,由于在fifo_with_scan.v网表里加入了扫描链（scan）逻辑，在验证之前，我们必须把这一扫描链（scan）逻辑功能禁止（disable）。进入Setup界面后，选择Constants，点击Set按钮，出现set Constant对话框。,设置SCAN链的功能无效,选择Implementation，

17、选择Instance的顶层fifo，在顶层fifo的ports目录下面搜索找到名为test_se（SCAN功能的使能信号）的管脚，在Constant Value中选择值0，设置test_se的值为0，点击OK按钮。,4.match,点击match，进入比较点（compare point）匹配步骤。点击Run Matching,运行运行结果：报告一个不匹配的compare point。点击ok，查看不匹配点。,选择Unmatched Points，可以看到报告栏里报告Implementation Object的test_se引脚不匹配。这个引脚是Implementation Design中多余的

18、compare point.我们在前一步骤里，已经把它禁止啦。故可以跳过这个不匹配点，进入下一步骤Verification。,5.verify,选择Verify，点击Verify All按钮，进行形式检查。运行结果如图：,结果报告如图：,检查RTL与GATE网表检查GATE网表和插入扫描链的GATE网表检查带有扫描链和JTAG链的GATE网表和插入扫描链的GATE网表,提 纲,三.检查fifo_with_scan_jtag.v和 fifo_with_scan.v一致性,fifo_with_scan_jtag.v是带有扫描SCAN链逻辑和JTAG链逻辑的网表文件 上一节中我们已经验证带有scan

19、的网表文件fifo_with_scan.v和fifo_mod.vg功能相同把fifo_with_scan.v作为参考设计，来检查fifo_with_scan_jtag.v的功能,和前面步骤一样，分别设置fifo_with_scan.v为Reference design,设置fifo_with_scan_jtag.v为Implementation design。,选择Setup，进入设置步骤。完成下面两个工作。禁止fifo_with_scan.v的scan的功能禁止fifo_with_scan_jtag.v的jtag的功能。,禁止scan和jtag功能,选择Constants，点击Set，进入设

20、置常量界面。选择reference的fifo的test_se引脚，设置test_se引脚值为0，禁止scan功能。选择Implementation的fifo的test_se引脚，设置test_se引脚值为0，禁止scan功能，选择Implementation的fifo的jtag_trst和jtag_tms引脚，设置这两引脚值为0，禁止jtag功能。,运行match,选择Match，点击Run Matching。运行结果如下：发现17个不匹配点，选择Unmatched Points，查看报告。发现Implementation Object这些不匹配点都是和jtag相关的。在前面一步骤里，我们已经禁止啦jtag功能。故可以跳过这些不匹配点。,Verify,选择Verify，点击Verify All,进行检查步骤。运行结果如下：,检查完毕，在fifo_with_scan.v网表里加入jtag链后，没有影响原来设计的功能。,