请教下FOMALITY，卡在verifying过程，是什么原因

第一张图是卡verifying的截图，跑了很久了。是RTL与网表对比。综合工具是DC

第二张图中如果注释这三行代码，重新综合。再跑FORMALITY不会卡verifying。

如果不注释，综合再跑FORMALITY就会出现第一张图中的卡verifying的情况。
第三张图是注释掉模块的代码，只是一个有限域的乘法运算，RTL仿真没有错误。

第四张图至第七张图是FORMALITY的脚本。

求大神帮我看看是什么原因卡verifying。谢谢了

自己顶一下

急，求大神解惑

再请教下

顶上去

没有大神吗

如何解决的?

这种数字运算的应该有命令来简化，具体命令要找下，否则formality会穷举将所有的条件比较，
这会比较时间很长

这叫state space explosion