Formality使用指南VIP免费

Formality使用指南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_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为referencedesign设置门级网表fifo.vg为Implementationdesign（一）图形用户界面进行形式验证在UNXI提示符下进入tutorial目录：输入fm（或formality）。1.设置referencedesign点击formality图形界面的reference按钮，进入ReadDesignFile点击Verilog按钮，出现添加Verilog文件的对话框。如下图：1.1读取源文件在对话框中选择：Rtl目录下的fifo.v文件，点击Open按钮,打开fifo.v源代码。如图：1.2设置搜索目录点击option按钮，出现setverilogreadoption对话框,选择Variable,在DesingWarerootdirectory(hdlin_dwroot)出输入：echo$SYNOPSYS或DesignCompiler的安装目录(本工作站的目录为/opt/tools/synopsys)，如下图：1.3设置搜索目录在Setverilogreadoption对话框中的VCSStyleOption中选择LibraryDirectory(-y),在EnterDiectoryName处浏览选择rtl目录然后点击add按钮添加查找目录rtl。选择LibraryExtension(-libext)，在EnterFileExtension处填上后缀名.v，然后点击add按钮添加，点击OK按钮。1.4加载源文件然后点击LOADFILES按钮，加载源文件fifo.v，如下图：1.5设置fifo为reference的顶层在点击SetTopDesign按钮，出现下图。在choosealibrary中选择WORK，在chooseadesign中选择fifo（顶层设计的模块名）在Setandlinkthetopdesign中点击SetTop，出现下图同时在Reference按钮上出现绿色的对号符：2.设置ImplementationDesign点击Implement按钮，在ReadDesignFiles中点击Verilog，出现Addverilogfiles对话框，选择gate目录下的verlog网表文件fifo.vg，点击LoadFiles加载网表文件fifo.vg，2.1加载Technologylibrary选择ReadDBLibraries按钮，点击DB…按钮，出现AddDBFiles对话框选择lib目录下的lsi_10k.db库文件，（确保Readassharelibrary被选中）点击LOADFiles，加载库文件。选择SetTopDesign,在Choosealibrary中选择WORK(DesignLibrary),在Chooseadesign中选择顶层模块名fifo，点击SetTop按钮。此时在Implementation出现绿色的对号符。3.设置环境(Setup)在这一步主要是设置常量，比如对应一些增加了SCAN扫描链和JTAG链的设计，需要设置一些常量，使这些SCAN和JTAG等功能的禁止。由于fifo.v是源代码，fifo.vg只是综合的源代码，没有添加SCAN和JTAG链。故可以省略这一步4.Match检查referencedesign和Implementiondesign的比较点是否匹配点击Match按钮，选择RunMatching按钮，进行匹配检查。出现下图结果：没有不匹配的比较点，可以进入下一步。5.Verify点击OK键，完成。现在你已经准备好，可以进行fifo.v和fifo.vg功能是否一致。选择Verify按钮，点击VerifyAll，进行形式验证。验证结束，结果出现“Verify”fail的对话框，提示两种功能不一致。6.Debug由于验证失败，系统直接进入DEBUG工作区。在FailingPoints的报告工作区里显示两设计的出不一致的比较点在FailingPoints的报告工作区内点击鼠标右键，选择ShowAllConeSize,在Size栏里显示每个comparpoint所包含的cell的数目一般调试是从cell数目最小的comparepoint开始。在这里我们从第一个comparepoint开始。选择r:/WORK/fifo/push_logic/full_flag/q_out_reg[o],击鼠标右键，选择菜单中的viewLogicCones，出现LogicConesView窗口。在这个新窗口里...