为什么形式验证失败

没有接触过后端，对DC也不熟悉。
这次项目中发现DC编译后的网表和RTL做形式验证，有两个模块的输出验证失败了。
特地来求教：
1、都是DC家的工具，为什么编译和形式验证会过不了？我原来以为，用自家的工具做形式验证是多余的，因为算法都一样，所以肯定能算出电路是一样的。
2、但是听说retiming会使形式验证失败，是真的吗？

还是程序问题!