生成覆蓋所需時間的意義

Question

我正式驗證大設計中的小模塊。

我已經分析和闡述了設計（使用Jaspergold -fpv）。

我寫了一個很簡單的蓋財產（SVA）爲：

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

大約需要5300秒找到蓋。我注意到「Bound」是143.

那麼爲什麼這需要這麼長時間來生成封面，這意味着什麼（時間和綁定）？

是否因爲該工具必須深入研究設計狀態才能生成覆蓋層並且COI很大？還是其他原因？

感謝您的幫助。

Answer 1

我發現了生成封面的處理時間很長的原因。長時間延遲的原因在於，形式引擎試圖（理想地）找到最短路徑來匹配特定的封面/序列。因此，在許多真實場景​​中，最短路徑可能不是正式引擎中最快的路徑。這是因爲，正式引擎可能不得不觸發大量觸發器才能達到特定的覆蓋狀態。

在我的特殊情況下，名爲'scan_mode'的觸發器依賴於幾個前面的觸發器。而且，因此該工具必須翻轉大量的觸發器才能使'scan_mode'有效。因此，觸發器上的假設屬性（1'b1）大大縮短了封面生成時間。 無假設屬性的封面生成時間：150秒。 具有假設屬性的封面生成時間：2秒。

Answer 2

試圖獲得可與signalA去斷言在CLK &的上升沿結束了所有的情況，因此根據COI

「綁定」所花費的時間說明，所有的組合試圖打去斷言signalA在143週期內完成。

總體而言，這些意味着有多少種方式可以使房產受到多大的衝擊。