Formality的RTL和网表对比出错

查了错误之后发现，是时钟选择模块出了问题。这个模块是一个三选一的MUX选择三个时钟中的一个。网表中确实是一个三选一的MUX，但是RTL里面显示的是一堆很奇怪的东西。所以想问一下Formality是什么原理将网表中的门和RTL的功能进行对比的?我这种情况可能的原因是什么?
谢谢！

有加上 DC 出来svf吗?
加上还不行就试下 set_case_analysis吧, 印象中不需要这句也可以比。

你好，我已经加上svf文件了。很奇怪，我单独综合了那个模块，是可以通过formality的，但是加进去就不行了。