数字IC设计学习笔记

Formality 形式验证

1. 基本特点
2. Reference Design 和Implementation Design
3. container
4. 读入共享技术库
5. 设置Reference Design
6. 设置Implementation Design
7. 保存及恢复所做的设置
8. 运行verify 命令

1. 基本特点：

Synopsys Formality 是形式验证的工具，你可以用它来比较一个修改后的设计和它原来的版本，或者一个RTL 级的设计和它的门级网表在功能上是否一致。

在IC设计中通常用于进行不同步骤的netlist的比较：逻辑综合netlist，floorplannetlist，placement netlist ，CTSinserted netlist,P&R netlist，在每一个步骤后都有新的逻辑加入到netlist中，但是这个新的逻辑的加入不能改变原netlist的l逻辑功能。

2. Reference Design 和Implementation Design：

形式验证的过程中涉及到两个设计：一个是标准的、其逻辑功能符合要求的设计，在Synopsys 的术语中称之为Reference Design；另一个是修改后的、其逻辑功能尚待验证的设计，称之为Implementation Design

3. container：

我们可以把container 理解为Formality 用来读入设计的一个空间，或者说一个“集装箱”，一般情况下要建立两个container 来分别保存Reference Design 和Implementation Design

4. 读入共享技术库：

在开始验证流程之前，首先要读入所有的会被用到的共享技术库

5. 设置Reference Design：

1）建立一个新的container；
2）读入门级网表；
3）确认该设计为Reference Design；
4）链接Reference Design；

6. 设置Implementation Design：

1）建立一个名为impl 的container，读入clk_insert1.v 文件；
2）确认Implementation Design；
3）链接该设计；
4）把该设计设置为当前设计，然后把其中的test_se 端口设置为0

7. 保存及恢复所做的设置

8. 运行verify 命令

Formality 将根据所作的设置，对ref 和impl 中的两个设计进行验证。

相比于动态仿真的优势在于：

不需要开发验证pattern
速度比较快
覆盖率100%
纯逻辑上的验证，不考虑物理和timing信息

缺点在于：

由于不考虑timing，因此需要配合STA工具使用。

— 转载内容源自知乎用户Amen, Thanks^^：https://zhuanlan.zhihu.com/p/73307269

【注】：个人学习笔记，如有错误，望不吝赐教，这厢有礼了~~~

数字IC设计学习笔记_Formality 形式验证相关推荐

数字IC设计学习笔记_静态时序分析STA_ STA基本概念
数字IC设计学习笔记 STA基本概念 1. STA基本概念 2. 时序弧概念 Timing Arc 3. 建立时间和保持时间概念 4. 时序路径概念Timing Path 5. 时钟域概念clock ...
数字IC设计学习笔记_静态时序分析STA_ PrimeTime 基本概述
数字IC设计学习笔记 PrimeTime 基本概述 1. PrimeTime 基本概述 2. 运行模式 1. PrimeTime 基本概述 PrimeTime,Synopsys公司提出的,针对于复杂的 ...
数字IC设计学习笔记_静态时序分析STA_伪路径False Paths
数字IC设计学习笔记半周期路径Half Cycle Path 1. 伪路径False Paths 2. 如何处理False Paths 1. 伪路径False Paths 在设计中,有些路径是不可能 ...
数字IC设计学习笔记（一）——逻辑综合简介
目录综合的抽象层次逻辑级(RTL)综合流程参考资料综合的抽象层次根据不同的抽象层次,综合可分为电路级综合.逻辑级综合.行为级综合电路综合将电路的逻辑翻译成满足性能要求的晶体管网表,包括使用 ...
Cadence IC设计学习笔记一
Virtuoso Schematic Editor学习启动建立新库.新单元及新视图添加元件添加管脚添加电源和地摆放元件并加网线层次化设计-symbol生成电路仿真创建激励信号电路模块 ...
数字IC前端学习笔记：LSFR（线性反馈移位寄存器）
引言 LSFR(线性反馈移位寄存器)用于产生可重复的伪随机序列PRBS(Pseudo-Random Binary Sequence),结构包括n级D触发器和一些异或门(或同或门)组成,在每个时钟沿,后 ...
模拟IC设计学习笔记（1）---恒流源负载的共源极放大器极点的观察与计算
一.电路设计 1.恒流源负载的共源极放大器模型 2.在本次电路仿真中我们设定的参数: pmos:W=L=5um nmos:W=L=2um 输出点放置1pF电容(较大,即忽略两个MOS管的漏端电容) ...
2023 数字IC设计秋招复盘——数十家公司笔试题、面试实录
最新更新日期:2023.04.02 1 目录/更新记录 1.1 笔试复盘篇按笔试的时间顺序进行更新.备注:笔试时间可能会与实际时间有偏差. 序号公司岗位链接笔试时间发布时间 0 禾赛 FP ...
笔试题-2023-燧原-数字IC设计【个人解答版】
回到首页:2023 数字IC设计秋招复盘--数十家公司笔试题.面试实录推荐内容:数字IC设计学习比较实用的资料推荐题目背景笔试时间:2022.07.07 应聘岗位:数字IC设计题目评价难易程 ...

数字IC设计学习笔记_Formality 形式验证

数字IC设计学习笔记

数字IC设计学习笔记_Formality 形式验证相关推荐

最新文章

热门文章