Formality使用指南手册.docx

目录说明 1(一)图形用户界面进行形式验证 (Setup) 13(二)命令行方式进行形式验证 13命令行方式运行 16设置SCAN链的功能无效 20禁止scan和jtag功能 20运行match 21Verify 21说明FiFo的Tutorial目录下包含以下几个子目录:Rtl:fifo的RTL源代码;,,,,,。Lib:门级网表需要的技术库;。Gate:综合的门级网表;。Gate_with_scan:插入扫描链的门级网表;。Gate_with_scan_jtag:带有扫描链和JTAG链的门级网表;。::(一)图形用户界面进行形式验证在UNXI提示符下进入tutorial目录:输入fm(或formality)。,进入ReadDesignFile,点击Verilog按钮,出现添加Verilog文件的对话框。如下图::,点击Open按钮,。如图:(上述源文件还未执行Loadfiles命令)点击option按钮,出现setverilogreadoption对话框,选择Variable,在DesingWarerootdirectory(hdlin_dwroot)出输入:echo$piler的安装目录(本工作站的目录为/opt/tools/synopsys),如下图:(-y),在EnterDiectoryName处浏览选择rtl目录,然后点击add按钮添加查找目录rtl。选择LibraryExtension(-libext),,然后点击add按钮添加,点击OK按钮。,,如下图:,出现下图。在choosealibrary中选择WORK,在chooseadesign中选择fifo(顶层设计的模块名)在Setandlinkthetopdesign中点击SetTop,出现下图同时在Reference按钮上出现绿色的对号符:,在ReadDesignFiles中点击Verilog,出现Addverilogfiles对话框,,,,点击DB…按钮,出现AddDBFiles对话框,,(确保Readassharelibrary被选中)点击LOADFiles,加载库文件。选择SetTopDesign,在Choosealibrary中选择WORK(DesignLibrary),在Choose