Formality形式化验证脚本范本
1、验证带DFT网表:首先要disable scan logic和Bist功能
2、可以将所有的代码、网表,包括所有的子模块、顶层的全部读入,在read过程中针对top使用set_top,有关环境设置不急于读入,完成后,可以保存该阶段性为*.fss格式文件(下次restore_session该文件即可,库、网表、设计不需要重复读入)。
脚本主要过程如下:
source ./variable.tcl#设计顶层、路径等变量设置
source ./target_lib.tcl#设计中用到的所以库文件,可能需要lib2db,链接:#http://blog.csdn.net/a670449625/article/details/72459459
#脚本内容:read_db "$LIB_PATH/lib_name.db ... ..."
source ./read.tcl#读入ref和impl设计
#脚本内容:read_verilog -container r -libname WORK $REF_LIST
#set_top r:/WORK/TOP
#read_verilog i:/WORK/TOP
#save_seesion r_i_load.fss
#此时采用自底向上的策略,假设顶层TOP下有两个子模块A和B
#验证子模块A
set_reference_design r:/WORK/A
set_implementation_design i:/WORK/A
current_design r:/WORK/A
source ./ref_setup.tcl#针对ref container的一些设置,eg:constants、black_box、dont_verify_points等
current_design i:/WORK/A
source ./impl_setup.tcl#针对impl container的一些设置,eg:constants、black_box、dont_verify_points等,涉#及到DFT、时钟树方面的,设置方面会多余针对ref的设置
match
set result [verify]#此时会显示出:Reference deisgn is 'r:/WORK/A' Implementation design is 'i:/WORK/A'
if (result ==0)
analyze_points -all > ./analyze_points.log#分析所有failing points
source ./report.tcl#打印验证结果,包括:failing、pasing points、user constants、report_status等等
else
source ./report.tcl
#至此,子模块A的验证工作完成,此时对fm_shell来说,停留在verify mode下
setup#将模式更改为setup
set_reference_design r:/WORK/B
set_implementation_design i:/WORK/B
#之后步骤类似子模块A,在子模块B验证完成后,fm_shell仍停留在verify mode下
setup
set_reference_design r:/WORK/TOP
set_implementation_design i:/WORK/TOP
source ./top_setup.tcl#将子模块A和B设置为黑盒子、Interface only等
#剩余步骤跟子模块验证相同。
Formality形式化验证脚本范本相关推荐
- 形式化验证工具TLA+:程序员视角的入门之道
简介: 女娲是飞天分布式系统中提供分布式协同的基础服务,支撑着阿里云的计算.网络.存储等几乎所有云产品.在女娲分布式协同服务中,一致性引擎是核心基础模块,支持了Paxos,Raft,EPaxos等多种 ...
- 国产自主可控的形式化验证代码自动生成工具ModelCoder可替代Matlab/Sumlink
在安全关键领域,基于模型的软件工程或者软件开发已逐渐进入了我国的装备研制过程中.使用SimuLink或者SCADE等嵌入式软件建模工具对算法或者控制逻辑进行可视化建模,然后生成高可靠的二进制代码逐渐成 ...
- 便携式三星mysql_三星集团某站点MySQL盲注一枚(附python验证脚本)
漏洞概要 缺陷编号:WooYun-2014-082219 漏洞标题:三星集团某站点MySQL盲注一枚(附python验证脚本) 相关厂商:三星集团 漏洞作者:lijiejie 提交时间:2014-11 ...
- 随想录(形式化验证小结)
[ 声明:版权所有,欢迎转载,请勿用于商业用途. 联系信箱:feixiaoxing @163.com] 形式化验证,英文是formal verification,是验证软硬件逻辑很重要的一种方法.特 ...
- Formality形式验证教程
Formality形式验证主要验证综合后,生成的网表文件功能和之前的verilog文件功能是否一致, 需要两个文件,一个verilog文件,一个是网表文件 1.新建一个文件夹,把verilog文件和网 ...
- linux内核形式化验证,说说形式化验证(Formal Verification)吧
原标题:说说形式化验证(Formal Verification)吧 前言:被@暴走恭亲王点名,不得不写这个小文,笔者学识浅薄,而形式化验证这个题目不但大,而且深,笔者掌握的数学知识在专业人士里也就是幼 ...
- linux内核形式化验证,聪明人的笨功夫 -- MesaTEE安全形式化验证实践
各类TEE(例如TPM和Intel SGX)提供了强大的可信计算硬件基础,但他们并不直接保证软件的安全性.诸如缓冲区溢出等内存安全问题为攻击者提供了侵入TEE的可乘之机.因此,软件内存安全保护极其重要 ...
- 操作系统形式化验证实践教程(7) - C代码的自动验证
操作系统形式化验证实践教程(7) - C代码的自动验证 上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
- 操作系统形式化验证实践教程(7) - C代码的自动验证(转载)
操作系统形式化验证实践教程(7) - C代码的自动验证 上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
- 鸿蒙 形式化验证,形式化验证在网络中的应用
作者简介:唐昊,现就职于华为,从事云网络研发工作. IBN(基于意图的网络)是近年来网络领域中最热门的话题之一,网络验证是其中最关键的环节.我们在此之前一直专注于网络配置的自动化,例如根据模板创建配置 ...
最新文章
- Iframe上传文件
- Linux进程与线程的区别 详细总结(面试经验总结)
- MySQL存储过程总结(二)
- close和SO_LINGER
- perl计算IP所在的子网范围
- oracle授权操作
- python画太极八卦图_太极八卦图的正确画法
- 【poj 2891】Strange Way to Express Integers(数论--拓展欧几里德 求解同余方程组 模版题)...
- 亚马逊的新Linux发行版对红帽造成了威胁
- 计算某天是星期几数字或文本形式的JAVA工具方法
- Bitmap头文件说明
- 冒泡排序和快速排序的区别
- python简单图片处理
- ubuntu16.04安装iNode客户端简易教程
- Week08手写笔记
- 云和恩墨入选《数据安全产品与服务图谱1.0》
- Web界面应用的测试内容
- 第8节 Kali及其他Linux系统软件分类及安装
- 哈工大威海计算机学院教师,计算机学院青年教师齐元凯在《IEEE T-PAMI》上发表论文...
- Linux 学习 第六单元