module compiler 之后formality出现问题，求助。

lanyiel

用module compiler生成的RTL和netlist，分别是.bvrl 和.vrl文件，但是当把.vrl再经过DC综合优化后，与原来的.bvrl进行比较，就会出现fail,有哪位达人，遇到过这个情况，怎么处理的。

haharun

原帖由 lanyiel 于 2009-8-26 12:46 发表

                               
登录/注册后可看大图

用module compiler生成的RTL和netlist，分别是.bvrl 和.vrl文件，但是当把.vrl再经过DC综合优化后，与原来的.bvrl进行比较，就会出现fail,有哪位达人，遇到过这个情况，怎么处理的。

First step, please check if original .bvrl  and .vrl can pass FV,
Second step, please check if your DC has e.g. ungroup or boundary optimization,
Basically I believe the key points have been modified during step 1) or 2)

lanyiel

多谢楼上的建议。
生成的.bvrl and .vrl是不一样的，FV也是fail，而且这种情况一般很多，因为如果有pipeline的时候，在DC那里要做retiming的，所以感觉这里是不可能equivalent的。
有没有办法解决这个问题呢。

haharun

原帖由 lanyiel 于 2009-8-27 11:55 发表

                               
登录/注册后可看大图

多谢楼上的建议。生成的.bvrl and .vrl是不一样的，FV也是fail，而且这种情况一般很多，因为如果有pipeline的时候，在DC那里要做retiming的，所以感觉这里是不可能equivalent的。有没有办法解决这个问题呢。

retiming给了DC最大的自由度， 但其后果就是FV很难compare。
这也是很多公司flow里不做retiming的原因，
我想你可以考虑把attribute设成black box, （如果你确信的话）
因为有些design, 比如一些除法器的designware， 天生FV就是比不过的。

其次， Formal的工具如果足够聪明， 应该也可以retiming RTL,
这样可以形成和DC retiming等价的key points,
但是这个涉及到工具问题， 你可以查查相关资料