综合后带门控时钟单元的网表和RTL做形式化验证问题

alphavor_jay · 发表于 2011-12-4 11:12:32

您需要登录才可以下载或查看，没有账号？注册

x

RTL经过DC综合后生成的时带门控时钟的网表,然后把这两个放到Formality里面做形式化验证,门控时钟输出相连的相关寄存器都会成为verify failed point,请问各位XDJM有没有碰到过这种情况呢?小弟先谢过了~

alphavor_jay · 发表于 2011-12-4 11:55:59

找到答案了,跟大家分享一下:
setup
set verification_clock_gate_hold_mode any

icfbicfb · 发表于 2011-12-4 13:28:15

这样的，多谢，好像是经常的问题

alphavor_jay · 发表于 2011-12-5 01:49:55

回复 3# icfbicfb

呵呵，用我们老大账号上sovnet上查到的，就跟大家分享一下，如果用形式化验证的话这个问题应该迟早会遇到的

guiqiguiqi · 发表于 2011-12-5 21:23:25

回复 2# alphavor_jay

你好你这句command 什么意思，如何使用？

alphavor_jay · 发表于 2011-12-5 21:26:12

回复 5# guiqiguiqi

setup
set verification_clock_gate_hold_mode any
这是两句command，我是直接在fm_shell -gui&调出来后的gui命令窗口中直接使用，也可以直接run script.

guiqiguiqi · 发表于 2011-12-5 21:42:53

回复 6# alphavor_jay

setup是一句command？看起来好奇怪啊。
是不是这两句command用了，FM进行对比的时候就无视clock gating了？

lunmag · 发表于 2013-6-9 06:57:56

这是在Setup 里面设置上这个命令吧，和设置常量是一样的

血溶伊剑 · 发表于 2015-11-5 13:31:00

学习了。

Haniel1986 · 发表于 2015-11-19 13:45:22

学习了！

[求助] 综合后带门控时钟单元的网表和RTL做形式化验证问题