formality debug summary

最近在formality上遇到一些问题，最终解决了。这里做一下总结记录。

问题起因是拿到一个unmapped *.ddc格式的设计输入。

对整个芯片的综合而言，可以使用*.ddc做输入，但formality怎么比呢？formality不支持读入未经compile过的ddc格式文件。

所以暂定的策略是使用*.ddc做输入，同时写出gtech网表和map到工艺库的网表（以及对应svf），对两个网表进行formality比较，确认一致性。

在这一步纠结了非常长的时间，因为设计本身有比较多的运算，一些比较大的DW模块比得很困难，最后剩下3%左右的points报的不是timeout就是abort。

在formality这块做了非常多的尝试：

• 分布迭代去做单个点的verify -> 迭代到最后剩1%，结果均为abort
• 按FM建议将set_verification_priority xxx加到DC script中 -> 对abort point并无改善
• 将set_parameter -retimed xxx 标到FM script中 -> 原始都综合工程中本身也没有被retime处理的电路，因此对abort point并无改善
• 在DC script中尝试全部打平设计(ungroup -flatten -all) -> 对比较效率有提升，对最终的abort point仍无改善
• 统一更新DC/FM到同一个版本号的最新版本 -> 结果无改善
• 去除掉DC script中多余的option，对于写出gtech网表和写出工艺库网表，均只保留最基本的setup lib->read design->compile->write file。结果仍然没有改善
• 基于hierarchy flow去做formality，一级一级向下排查 -> 因为子模块比较多，这个实验没有完全走下去，但是排查到有些DW mult模块的比较会报abort，但也有一些DW mult模块是可以pass的。

其实这个时候已经有些猜测，因为拿gtech网表比工艺库网表，两边都是网表，但svf只能吃到工艺库一边的svf。所以如果gtech网表有一点点的过优化，都可能会导致比较fail。

在做新的一轮实验的时候，进一步精简写出gtech网表的script，在setup_lib这一步时直接set link_library [list *]，去掉了设置里面的dw_foundation.sldb. 结果这次写出的gtech网表居然比较通过了。

从DC的log里面可以看到，不带dw_foundation.sldb的话，DC会调用默认的Basic DW Building Blocks，处理DW子模块时的log为”Process xxx ….”. 加上dw_foundation.sldb之后，DC会调用Licensed DW Building Blocks，处理DW子模块时的log为“Mapping xxx …”.

写了一个简单的乘法模块去做实验。发现BasicDW vs. LicensedDW二者综合出来的电路果然是不一样的。把他俩放到formality里去作比较，结果很有意思：

• 当乘法器规模较小时，二者综合出来的网表电路有较少差异，formality比较还可以pass。
• 当乘法器规模较大时，二者综合出来的网表电路差异也较大（hierachy都不一样了），formality比较也会fail或abort。

这个结果看起来跟前面hierachy check结果也是match的。

---

ps.最后说一下，为什么不拿gtech网表再去综合写一个工艺库网表出来，直接这样比呢？

• 因为前期综合的时候script里都带了dw_foundation.sldb. 一旦拿使用LicensedDW综合得出的网表同用LicensedDW的gtech网表比formality的话，就会跑出abort的结果。
• 而前期直接使用gtech网表的时候，在full chip综合后得到的timing十分差，面积也要大很多。基于这两方面考虑，没有直接使用gtech网表作为全芯片综合的设计输入。
• 后来在dw_foundation.sldb的问题揭开后，作为对照实验，用整理过的DC script（不带dw_foundation.sldb）重跑了gtech网表和基于gtech网表的工艺库网表，二者formality也能比过，timing看上去也没有很差。

---

其他一些值得一提的小tips:

• 综合输入中有ddc文件时，需要在link_library中加”*”，这样ddc内部的sub module才能被link上。
• 综合如果gtech库没设置好，写出的网表会包含SEQGEN。
• link_library中强制要求包含target_library和synthetic_library，但synthetic_library可以为空。target_library不可为空。
• 使用compile_ultra的话，会强制要求dw_foundation.sldb库。不加的话会报错。
• 写rtl的时候，可以直接写+-*/。综合工具会自己把运算映射到到相应的DW单元。如果考虑复用节省资源的话，可以手动选择DW例化到rtl里面（或者把+-*/相关的处理写成小模块，在上一层例化的接口处做mux）。
• fpga需要的gtech.v可以去synopsys/fpga/…目录下面找。是一个完全RTL描述的文件。synopsys/syn/…目录下面找到的会是原语描述文件，仿真没问题，但是fpga不识别。