代码编织梦想


前言

由于项目后期需要完成一个rtl和网表之间的形式验证,需要用synopsys的formality来完成,由于第一次接触,也摸索了将近三天才能上手使用,记录一下整个flow的过程

一、formality是什么?

formality是S家的形式验证的工具,形式验证故名思意是完成一个表面逻辑的验证,通过导入rtl代码和DC综合后的门级网表,验证前后逻辑是否一致,是否DC将部分逻辑消除了。

二、使用步骤

0.打开formality的gui界面

在这里插入图片描述
只需要在终端输入formality就可以打开gui界面了

1.导入svf文件

在这里插入图片描述

svf文件是DC综合过程中产生的文件,用来记录DC对网表产生的一些变化,防止后续的rtl和门级网表对应不上的问题。

2.读入verilog文件

在这里插入图片描述
第二步就是读入rtl级代码了,但是此处需要注意两点

  • 一.是否用到了IP,如果用到了IP,那么不需要在read design files 中将verilog代码读入,而是在后续的read DB libraries 中读入IP的db文件即可。

  • 在这里插入图片描述

  • 二.是否在design中直接用到了工艺库中的module,如果用到了需要在options中设置。 具体如下图

在这里插入图片描述

  • 首先在options中的variables的designware root directroy中选择DC安装的路径。

在这里插入图片描述

  • 然后在VCS style options选项卡中的library file中选择应用的工艺库的.v文件,并add
  • 最后在set top design中选择顶层module进行set top,成功后ref上会出现绿色小勾。

3.读入网表文件

在这里插入图片描述
在impl栏中同样也是读入design 和 db ,只不过这里要读的是网表的design和db,
和步骤二类似,如果调用了pdks的设计,也要在options中设置,而db读入过程中除了要读入IP的db,还要读入pdks的db。最后设置set top,成功后同样会出现绿色小勾

4.setup

setup好像是为了带有扫描链和DFT的设计准备的,本人暂时还没用过

5.match and verify

全部设置完就可以,mathc and verify了,如果通过的话会提示verify succeed。如果失败的话会具体提示哪些部分验证不上。比如

在这里插入图片描述

6.注意事项

这里有一个很重要的点,DC 的set_svf一定要放在脚本最前面,否则有些改变不会记录下来,我就是因为这个原因有两个FF一直unmatch,还以为是latcg的问题,其实
set verification_clock_gate_edge_analysis true
这条语句可以将DC生成的latcg作用屏蔽。

版权声明:本文为博主原创文章,遵循 CC 4.0 BY-SA 版权协议,转载请附上原文出处链接和本声明。
本文链接: https://blog.csdn.net/sz_woshishazi/article/details/108621525

synopsys formality workshop 2013-爱代码爱编程

四月底忙里偷闲去参加了为期两天的Formality的workshop。讲师还是那个讲师,不过相比于2010年底的听的那次Formalityworkshop2005,内容有很大的调整和更新,尤其是使用Formality的策略和debug的各种方法技巧,都总结的比较清晰、可操作。推荐有机会去的同学们再去听一下。 有个小道消息是,Synopsys也正在开

formality的一点经验总结_亓磊的博客-爱代码爱编程_formality loop

文章目录 一、 总结:二、 netlist和svf的配套一致三、 formality遇到的坑四、 pattern match视角五、 IP/IO/standcell的处理 一、 总结: 解决dc综合出现fai

形式验证 formality的设置及fm_shell使用_cy413026的博客-爱代码爱编程_verification_clock_gate_hold_mode

形式验证进阶(二):Setup阶段的约束信息&说说formality中比较点匹配 2018-10-26  芯司机  公众号:chipdriver 之前的文章导读 《形式验证入门之基本概念和流程》 《形式验证进阶(一):Guidance&Load Design》 Setup阶段的约束信息 1.常规setup设置 1)如果DC的综合脚本中

formality软件使用教程-爱代码爱编程

(参考:https://mp.weixin.qq.com/s/XznSbJBlAdZvtAIpyzajAA) 一、formality简介 在现在的数字集成电路设计流程中,有很多步骤都需要进行验证。随着数字集成电路的规模、复杂度,以及在验证过程中需要的仿真矢量的不断增加,用传统的仿真器进行验证越来越成为整个设计过程中的瓶颈之所在。 所谓形式验证,就是通过

Formality流程-爱代码爱编程

Formality流程 前言一、formality是什么?二、使用步骤0.打开formality的gui界面1.导入svf文件2.读入verilog文件3.读入网表文件4.setup5.match and verify6.注意事项 前言 由于项目后期需要完成一个rtl和网表之间的形式验证,需要用synopsys的formality来完成,由于

synopsys的rm流程_IC后端流程(初学必看).pdf-爱代码爱编程

校外IC后端实践报告本教程通过对synopsys公司给的lab进行培训,从verilog代码到版图的整个流程(当然只是基本流程,因为真正一个大型的设计不是那么简单就完成的),此教程的目的就是为了让大家尽快了解数字IC设计的大概流程,为以后学习建立一个基础。此教程只是本人探索实验的结果,并不代表内容都是正确的,只是为了说明大概的流程,里面一定还有很多未完

synopsys的rm流程_Synopsys工具简介(转)-爱代码爱编程

〓 LEDA LEDA?是可编程的语法和设计规范检查工具,它能够对全芯片的Vhdl和verilog描述、或者两者混合描述进行检查,加速SoC的设计流程。 LEDA预先将IEEE可综合规范、可仿真规范、可测性规范和设计服用规范集成,提高设计者分析代码的能力 〓 VCSTM VCS是编译型Verilog模拟器,它完全支持OVI标准的Verilog H

synopsys的rm流程_synopsys设计流程-爱代码爱编程

Synopsys 推荐设计流程 设计规范检查 1. LEDA 设计综合 ≤ 0.18um 0.18 - 0.35um 可测性设计 低功耗设计 FPGA 综合 5.Physical Compiler 6.ClockTree Compiler 7.DC-Expert 8. DC-Ultra 9. DFT Compi

【转载】Synopsys 推荐的 UPF 流程简介-爱代码爱编程

转载自http://blog.eetop.cn/blog-1561828-5940203.html 一、什么是UPF?   UPF的全称是统一功耗格式(UnifiedPower Format),其主要是由Synopsys推出的专门用于描述电路电源功耗意图的一种语言标准,它是Tcl语言的扩展,并且现在已经成为IEEE-1801标准且被三大EDA厂商(Syn

关于RISC-V的介绍与CPU设计-爱代码爱编程

目录 什么是RISC-V什么是什么名校优生他怎么就那么招人待见CPU设计入门CPU设计流程CPU的设计大纲总结最后本人自己的一句话预告 大家好我是木林!由于个人的比赛和项目问题已经有连续一个多月没有真正的静下心来去输出一些内容了,接下来由于项目问题或许时间会更少,虽然只有十几个粉丝 也是感觉对不住大家当然目前我已经有两个完成的项目了,这两

SYNS formality 形式验证常见debug 步骤-爱代码爱编程

formality 是synopsys 用来验证两个design是否等价的工具,也是IC实现中sign off tool,常用在design ECO 验证,tptg 前后由于design hierarchy变动的功能一致性验证,以及DC综合/DFT insert (OCC/SMS ) /PR(布局布线) 前后 design的function (功能等价性)