为什么Encounter Conformal在设计的正式验证期间报告不匹配,包括lpm_counter宏功能?

形式验证失配导致产生的设计包括lpm_counter宏功能时lpm_counter宏功能的两个或更多个异步控制信号(ASET,ACLR,aload)被使用。

为了消除这些不匹配,编译设计之前申请黑匣子属性在Quartus®II软件lpm_counter宏功能的包装。

有关使用Conformal进行形式验证的更多信息,请参考Quartus II手册第3卷中的Cadence Encounter Conformal Support (PDF)章节。

编辑 重设标签(回车键确认) 标为违禁 关闭 合并 删除

提问于 2018-08-04 14:29:55 +0800

这个帖子被标记为一个社区wiki

这个帖子是一个wiki(维基). 任何一个积分 >500的人都可以完善它