rtl代码里例化了库里的一个module，综合和形式验证的时候应该怎么做

ZHZIC

在RTL代码里例化了库里的一个module，综合的时候需不需要加进去库里的。v文件，只加DB文件可以吗？
形式验证的时候，需要加把库里的。v文件加进去，还是加上DB文件

jake

综合不需要加库的 .v.  综合script 已经给了库的 .lib 或  .db, 工具知道在哪里找到这个 cell，工具也知道这个 cell 的功能。
形式验证是 formal verification 吗？ 如果是，要给库的 .v, 这样工具才能知道这个 cell 的功能。

jake

看了前一个帖子，原来指的是 Formality， 应该是 LEC (logic equivalence check).
Formality 肯定能识别 ICG 的。 跑 Formality 应该给库的 .lib，Formality 肯定是能理解每一个 cell 的功能的。
Formality 报错很多时候是设置不对，如没有 disable ATPG，没有给 ATPG 有关的 ports 加上 constraint.
ICG 的 TE pin 在 RTL 里应该用 atpg_mode 去 drive

ZHZIC

   

jake 发表于 2020-10-23 02:10
综合不需要加库的 .v.  综合script 已经给了库的 .lib 或  .db, 工具知道在哪里找到这个 cell，工具也知道 ...

就是综合之后的网表和RTL代码进行验证，输入RTL代码的时候，是需要.V文件的嘛？

主要是我看到读完rtl之后，有Read DB Libraries这个选项，所以我怀疑这个就是在暗示我要用db文件
我知道第二步Impl肯定是要用db文件的

jake

   

ZHZIC 发表于 2020-10-22 12:31
就是综合之后的网表和RTL代码进行验证，输入RTL代码的时候，是需要.V文件的嘛？

主要是我看到读完rtl之 ...

给 .db 或 .lib 就可以了。
建议还是写个 script，command 有更多参数可加，直接明了，比 GUI 灵活多了。

ZHZIC

   

jake 发表于 2020-10-23 02:18
看了前一个帖子，原来指的是 Formality， 应该是 LEC (logic equivalence check).
Formality 肯定能识别 I ...

最后一句没看懂。。。
TE pin具体应该怎么操作，在哪一步？
我在rtl里面直接让它等于0了

jake

   

ZHZIC 发表于 2020-10-23 01:26
最后一句没看懂。。。
TE pin具体应该怎么操作，在哪一步？
我在rtl里面直接让它等于0了

没有 scan chain, TE tie to 1'b0 是对的。