| |
一、形式验证
形式验证是什么?什么时候做形式验证?这两个问题算是形式验证的核心问题。第一个问题有关于形式验证的理论,第二个问题有关形式验证的实际应用。
形式验证是为了验证RTL代码与门级网表之间的逻辑等价性。通常在综合的流程中会插入扫描链(关于可测性设计将在后续文章中进行介绍),这样综合出的结果的逻辑关系可能会与RTL代码的等效逻辑不一致;在版图流程中,通常会做时钟树综合,将会在网表中插入BUFF和反向器,这就可能会造成逻辑的不等价。如果在这两种情况下,都采用重新进行一番验证的方式来验证门级网表的正确性,那么将会带来大量的时间消耗,项目流程会被拉长,这对于IC设计来说是不能承受的高成本,因此,采用逻辑等价性验证的方式来验证综合之后、版图导出的门级网表是否与经过验证的RTL代码的逻辑功能完全等价。这样就使得综合之后的门级网表在节省时间的前提下,得到完全的功能验证。
形式验证流程主要是在综合插入扫描链之后,版图时钟树综合之后进行。
二、工具
形式验证工具有很多中,常用的有Formality,conformal(cadence公司),本章节将采用Formality。
三、示例
利用上一章节(综合)产生的门级网表文件,以及原始RTL代码文件,本示例给出一个简单的教程。
所需文件,如下图所示,其中,UART_XMTR_m.v为综合产生的网表文件:
启动formality图像化界面,启动命令:formality
步骤1,Ref载入参考文件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”
步骤3,Impl载入待验证门级网表,流程与步骤1一致,注意选项卡的选择,如下图,
步骤4,4.Match,5,Verify, “Run matching > ok,”“verify > OK”
步骤6,查看formality运行的终端信息,看到Verifiction SUCCEEDED,表明验证成功,如果不成功,那就要慢慢找原因了。回到6.debug中,可以看到failling points栏是空的,没有不匹配的地方。
以上就是formality验证的一般流程,由于这个流程没有在综合的时候插入扫描链,所以验证之后没有不匹配点,也就没有debug的必要。但是,在实际应用中,一定会存在不匹配点,这个时候就需要仔细的debug了。