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

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

First step, please check if original .bvrland .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)

多谢楼上的建议。
生成的.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,
但是这个涉及到工具问题， 你可以查查相关资料