请教个Formality的问题

时间：10-02 整理：3721RD 点击：

在做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，怕影响别的地方
谢谢！

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

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

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

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

毫无疑问，该rtl

上一篇：vcs求助！
下一篇：求助：xilinx ise 10.1 无法产生测试基准波形文件

FPGA ASIC quartus Xilinx vivado verilog ALTERA CPLD 集成电路相关文章：

栏目分类