Asic设计学习总结-形式验证

上一篇 / 下一篇  2018-03-07 20:01:48

一、形式验证

形式验证是什么?什么时候做形式验证?这两个问题算是形式验证的核心问题。第一个问题有关于形式验证的理论,第二个问题有关形式验证的实际应用。

形式验证是为了验证RTL代码与门级网表之间的逻辑等价性。通常在综合的流程中会插入扫描链(关于可测性设计将在后续文章中进行介绍),这样综合出的结果的逻辑关系可能会与RTL代码的等效逻辑不一致;在版图流程中,通常会做时钟树综合,将会在网表中插入BUFF和反向器,这就可能会造成逻辑的不等价。如果在这两种情况下,都采用重新进行一番验证的方式来验证门级网表的正确性,那么将会带来大量的时间消耗,项目流程会被拉长,这对于IC设计来说是不能承受的高成本,因此,采用逻辑等价性验证的方式来验证综合之后、版图导出的门级网表是否与经过验证的RTL代码的逻辑功能完全等价。这样就使得综合之后的门级网表在节省时间的前提下,得到完全的功能验证。

形式验证流程主要是在综合插入扫描链之后,版图时钟树综合之后进行。

二、工具

形式验证工具有很多中,常用的有Formalityconformal(cadence公司),本章节将采用Formality

三、示例

利用上一章节(综合)产生的门级网表文件,以及原始RTL代码文件,本示例给出一个简单的教程。

所需文件,如下图所示,其中,UART_XMTR_m.v为综合产生的网表文件:

启动formality图像化界面,启动命令:formality

步骤1Ref载入参考文件RTL代码,“verilog... > 选中files框下的文件 > loadfile > 3.Set Top Design选项卡 > 2.Choose a design UART_XMTR > Set top

 

步骤2,载入综合库,“2.Read DB Libraries > DB.. 选择综合库/home/Lance/synopsys/model/018SC7/SM00LB501-FE-00000-r0p0-00rel0/aci/sc-m/synopsys/tt_1v8_25c.db > LoadFiles

步骤3Impl载入待验证门级网表,流程与步骤1一致,注意选项卡的选择,如下图,

 

 


步骤44.Match5Verify, Run matching > ok,”“verify > OK

 

 

步骤6,查看formality运行的终端信息,看到Verifiction SUCCEEDED,表明验证成功,如果不成功,那就要慢慢找原因了。回到6.debug中,可以看到failling points栏是空的,没有不匹配的地方。

 

 


 

以上就是formality验证的一般流程,由于这个流程没有在综合的时候插入扫描链,所以验证之后没有不匹配点,也就没有debug的必要。但是,在实际应用中,一定会存在不匹配点,这个时候就需要仔细的debug了。


TAG:

 

评分:0

我来说两句

显示全部

:loveliness: :handshake :victory: :funk: :time: :kiss: :call: :hug: :lol :'( :Q :L ;P :$ :P :o :@ :D :( :)

日历

« 2018-09-23  
      1
2345678
9101112131415
16171819202122
23242526272829
30      

数据统计

  • 访问量: 17330
  • 日志数: 26
  • 建立时间: 2017-05-17
  • 更新时间: 2018-03-07

RSS订阅

Open Toolbar
博聚网