formality一问

设计中有几个跨时钟域的信号做了双寄存器同步之后与原设计相比，用formality reference和implementation分别载入修改前后的设计，compare能成功吗？

formal对这些不怎么敏感，有clock gating的话要完全match不太可能

实验结果是：
普通数据双寄存器同步，增加的双寄存器会成为unmatched点，但是verify成功！
rst做同步释放处理，unmatched、verify failed！