请教关于formality读入svf文件的问题

dc中要自己写入

set_svf ./svf_path/冲唯design_top_name.svf

在fm_shell中，在制定set_svf是dc指定的路径就行了弊判棚。

可以在dc中输入set_svf off 就不用关租则闭dc terminal直接进行fm

找到问题所在了。

运行唯庆缓完DC后Terminal的退出需要使用exit指令退出到linux-shell，这样svf文件就可以读入了；直接关闭终端（此时DC正指模常结束，但停留在DC命令环境下）时，svf文件差早就无法读入。

Formality 形式验证

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工具使用

---