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

nickysy · 发表于 2016-1-13 14:21:47

您需要登录才可以下载或查看，没有账号？注册

x

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

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

如果不注释，综合再跑FORMALITY就会出现第一张图中的卡verifying的情况。

第三张图是注释掉模块的代码，只是一个有限域的乘法运算，RTL仿真没有错误。

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

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

nickysy · 发表于 2016-1-13 14:48:41

自己顶一下

nickysy · 发表于 2016-1-13 15:24:54

急，求大神解惑

nickysy · 发表于 2016-1-13 21:20:53

再请教下

nickysy · 发表于 2016-1-14 14:46:08

顶上去

nickysy · 发表于 2016-1-15 11:41:43

没有大神吗

njuptxie · 发表于 2016-3-23 13:37:37

如何解决的？

mandrake · 发表于 2017-12-5 22:38:35

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

Timme · 发表于 2017-12-5 23:25:39

这叫state space explosion

yangxuchen · 发表于 2023-1-28 16:57:38

请问解决了吗？

[求助] 请教下FOMALITY，卡在verifying过程，是什么原因