请教个Formality的问题

airland · 发表于 2010-12-30 14:54:25

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

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

x

在做RTL和Gate的module level Formality验证，由于后端做了些优化，导致这个module的output在Gate netlist里面被加了个反相器然后才输出，就像下面这个样子：
RTL：A_OUTPUT = DFF.Q
Gate: A_OUTPUT = ~(DFF.Q)

这样RTL和Gate必然不等，这种情况怎么处理呢？直接set_dont_verify也不是很合适，因为这个output在这个module外面有load，怕影响别的地方
谢谢！

creese · 发表于 2010-12-30 15:20:03

这个register的output在进入load之前如果只是加了一个反相器，那就是错误的，这就相当于改变了这两个register之间的逻辑功能了。

creese · 发表于 2010-12-30 15:22:00

你做这个formality的目的就是找出post-netlist与RTL之间功能的不同，而不是想办法让其通过，找到不同后找出原因自然就通过了，所以通过是结果，而不是目的。

airland · 发表于 2010-12-30 15:43:46

感谢回复啊
情况是这个样子的，这个output在set_top的这个module里面没有load，在这个module的外面有load，后端的工具出于某种考虑，在这个module的里面将这个信号先反向、然后再输出了。所以，从整个chip的功能来讲，是没有问题的。问题是我现在做的是这个module的形式验证，所以要考虑怎么处理这样的output

这个register的output在进入load之前如果只是加了一个反相器，那就是错误的，这就相当于改变了这两个regist ...
creese 发表于 2010-12-30 15:20

登录/注册后可看大图

creese · 发表于 2010-12-30 16:57:30

那就在做这个module时dont verify，然后做top层次时再verify

macaren · 发表于 2011-1-15 15:18:32

毫无疑问，该rtl

[求助] 请教个Formality的问题

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

相关帖子

站长推荐 /2