前言

由于项目后期需要完成一个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作用屏蔽。

搜索关注我的微信公众号【IC墨鱼仔】，获取我的更多IC干货分享！

Formality流程相关推荐

Formality使用总结1
formality流程总结1 一.图形界面启动方式在命令行输入formality,接着可以看到如下界面以下1~6为进行formality的流程 0.Guid 在这一步导入DC综合产生的.svf文件 ...
Synopsys Formality 2018操作流程
Synopsys Formality 2018操作流程王_嘻嘻 2020-09-16 15:20:18 1940 收藏 26 分类专栏: eda工具使用经验文章标签: verilog 版权声明:本 ...
formality: 形式验证流程
formality工具作用于设计开发过程中验证逻辑功能是否产生变化,不考虑layout与timing,可以作为动态仿真的替代品.受制于设计规模,仿真的时间与其输入向量的多寡有关,而formal ver ...
【ASIC设计】ASIC设计流程
项目策划形成项目任务书(项目进度,周期管理等). 流程:[市场需求--调研--可行性研究--论证--决策--任务书]. 系统说明及行为描述确定设计对象和目标,进一步明确芯片功能.内外部 ...
数字IC设计流程总结
IC设计是一个很复杂漫长的过程,笔者以下图进行总结,其中后端总结的很模糊,后续了解学习后再进行补充.笔者会根据自己的理解,一步步的分享自己理解的设计流程.其中难免有问题错误,望同学老师指出,感谢!哔哩 ...
芯片开发流程对应的三大EDA厂商工具
(EDA工具未完待续) Synopsys: 1.spyglass:CDC相关工具.CDC,跨时钟域设计,是设计工作中很重要的技术点. 2.VCS工具:verilog仿真工具. 3.design com ...
【数字IC基础知识1之数字芯片设计流程
一,数字芯片设计流程数字芯片设计分为前端设计和后端设计,其中前端(又称逻辑设计)包括以下部分: 1,需求分析 2,功能架构设计 3,RTL代码设计 4,功能仿真验证(前仿) 5,逻辑综合 6,静态时 ...
SYNS formality 形式验证常见debug 步骤
formality 是synopsys 用来验证两个design是否等价的工具,也是IC实现中sign off tool,常用在design ECO 验证,tptg 前后由于design hierar ...
formality软件使用教程
(参考:https://mp.weixin.qq.com/s/XznSbJBlAdZvtAIpyzajAA) 一.formality简介在现在的数字集成电路设计流程中,有很多步骤都需要进行验证.随着 ...

Formality流程