2

我正在正式验证大设计中的小模块。

我已经分析并详细说明了设计（使用 Jaspergold -fpv）。

我写了一个非常简单的封面属性（SVA）：

    cover_property1:cover property(@(posedge clk) $fell(signalA));

找到封面大约需要 5300 秒。我注意到“Bound”是143。

那么为什么生成封面需要这么长时间，这意味着什么（所用时间和限制）？

是否因为该工具必须深入研究设计状态才能生成封面并且 COI 很大？还是其他什么原因？

谢谢你的帮助。

4

2 回答 2

1

尝试获取所有可能最终导致在 Clk 上升沿上取消断言 signalA 的场景，因此所花费的时间取决于 COI

“Bound”表示所有试图击中取消断言信号 A 的组合都在少于 143 个周期内完成。

总体而言，这些都表明财产受到打击的方式和速度有多快。

于 2017-03-07T09:34:42.793 回答
1

我发现了生成封面的处理时间长的原因。长时间延迟的原因是正式引擎试图（理想情况下）找到匹配特定覆盖/序列的最短路径。因此，在许多实际场景中，对于正式引擎而言，最短路径可能不是最快的。这是因为，正式引擎可能必须切换许多触发器才能达到特定的覆盖状态。

在我的特殊情况下，名为“scan_mode”的触发器依赖于几个先前的触发器。并且，因此该工具必须翻转大量触发器才能断言“scan_mode”。因此，触发器 (1'b1) 上的假设属性大大减少了覆盖生成时间。没有假设属性的覆盖生成时间：150 秒。使用假设属性覆盖生成时间：2 秒。

于 2017-03-09T08:08:15.680 回答