VC Formal FPV 启动脚本简单模板

VC Formal(下简称VCF)工具是Synopsys厂开发的一个用于静态分析验证的商业EDA工具。

VCF有很多种应用模式，比如FRV(Formal Register Verification), FPV(Formal Property Verification), FCA(Formal Coverage Analysis), SEQ(Sequential Equivalence Checking)等等。

本文主要介绍FPV的启动脚本。FPV是基于断言属性的静态检查。相对于动态仿真验证，其优势在于能够遍历所有的输入可能性。

启动命令：vcf -f ./start_fpv.tcl 如果想要GUI模式启动，可以用vcf -verdi -f ./start_fpv.tcl启动

================ start_fpv.tcl ================

set_app_var fml_mode_on true ## 设置VCF工作模式

read_file -top dut -format sverilog -sva -vcs {-full64 -sverilog -f ../filelist/dut.f -f ../filelist/tb.f +define+......} ## 读取源文件进行编译

create_clock LCLK -period 833 ## 创建时钟

create_clock FCLK -period 555

create_reset RESETn -low ## 创建复位

set_constant PWROK -value 1 ## 设置常量信号

sim_run -stable ## 让Formal run若干个cycle, 达到稳定的初始状态

sim_save_reset ## 保存初始状态

check_fv ## 开始做断言属性静态检查

report_fv -list ## 报告静态检查的情况

save_session ##保存数据库，以后可以用vcf -restore直接打开

===============================================

可以将DUT相关的文件路径在dut.f中指定，将断言等平台相关的文件在tb.f中指定。断言可以通过bind的方式绑定到DUT中。可以写个xxx_bind.sv并加入到tb.f中。

============== xxx_bind.sv =========

bind dut assertion_module assert_inst(

.clk(sys_clk),

.reset(sys_reset),

......

);

.....

================================

上面的例子中，dut是module名，assertion_module是断言模块的module名，assert_inst是断言模块的例化名。bind实现的功能就是相当于在DUT模块内部例化一个断言模块，并按指定的关系进行信号绑定。比如上面这个例子，就是将DUT的sys_clk信号与断言模块的clk信号进行了绑定，将DUT的sys_reset信号与断言模块的reset信号进行了绑定。

VC Formal FPV 启动脚本简单模板相关推荐

mysql开机启动脚本_centos简单的mysql开机自启和自动保存脚本
1.备份写一个testdbbackup.sh文件 ------------------------ #!/bin/sh DBName=test DBUser=root DBPasswd=root B ...
WebLogic启动与简单项目配置
http://tlinle.blog.51cto.com/251944/839666 一WebLogic简介 webserver是用来构建网站的必要软件.可用来解析.发布网页等功能,它是用纯java开 ...
Windows XP启动脚本
Windows XP启动脚本(startup scripts)是计算机在登录屏幕出现之前运行的批处理文件,它的功能类似于Windows 9×和DOS中的自动执行批处理文件autoexec.bat.利用 ...
ubuntu 设置开机执行脚本_ubuntu-18.04 设置开机启动脚本
ubuntu-18.04 设置开机启动脚本参阅下列链接 ubuntu-18.04不能像ubuntu14一样通过编辑rc.local来设置开机启动脚本,通过下列简单设置后,可以使rc.local重新发 ...
Android启动脚本init.rc(2)
在Android中使用启动脚本init.rc,可以在系统的初始化中进行简单的操作. init.rc启动脚本路径:system/core/rootdir/init.rc 内容: Commands:命令 ...
通过Shell开发企业级专业服务启动脚本案例（MySQL）
老男孩教育Linux高端运维班Shell课后必会考试题: 企业Shell面试题10:开发企业级MySQL启动脚本说明: MySQL启动命令为: /bin/sh mysqld_safe --pid-f ...
linux开机启动脚本的顺序
如果 [url=javascript:;]服务[/url] 器重启之后需要手工开启许多服务.工作及以后的维护相对比较繁琐.特地总结了下 [url=javascript:;]linux[/url] ...
linux 启动脚本 tty,Linux启动过程简介
许多人对Linux的启动过程感到很神秘,因为所有的启动信息都在屏幕上一闪而过.其实, Linux的启动过程并不象启动信息所显示的那样复杂,它主要分成两个阶段: 1.启动内核.在这个阶段,内核装入内存并 ...
关于Ubuntu运行级别、开机启动脚本的说明
关于Ubuntu运行级别.开机启动脚本的说明目录简介 1.1介绍Ubuntu下面的自启动脚本目录 1.2 Linux操作系统运行级别的概念 1.3关于操作系统自启脚本的启动顺序 1.4 Lin ...

VC Formal FPV 启动脚本简单模板

VC Formal FPV 启动脚本简单模板相关推荐

最新文章

热门文章