生成封面所用时间的重要性

Question

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

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

我写了一个很简单的封面属性(SVA) as:

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

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

那么为什么生成封面要花这么长时间，这意味着什么（花费的时间和时间）？

是不是工具要深入设计状态生成封面，COI大？还是其他原因？

感谢您的帮助。

Answer 1

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

"Bound" 表示所有尝试击中取消断言信号 A 的组合都在不到 143 个周期内完成。

总体而言，这些表示 属性 命中的方式和速度。

Answer 2

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

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