カバーの生成に要する時間の意義

Question

私は大きなデザインの小さなモジュールを正式に検証しています。

私は（Jaspergold-fpvを使用して）そのデザインを分析し、精緻化しました。

ように私は非常に単純なカバープロパティ（SVA）を書いた：それはカバーを見つけるために周り5300秒かかり

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

。私は "束縛"が143であることに気づいた。

なぜ、これはカバーを生成するのに時間がかかり、これは何を意味するのか？

これは、ツールがカバーを生成するために設計状態を深く見なければならないため、COIが大きいからですか？それとも別の理由？

ありがとうございました。 Clkの&のsignalAにデアサート立ち上がりエッジで終わることができるすべてのシナリオを取得する

Answer 1

カバーを生成するための処理時間が長い理由がわかりました。長い遅延の理由は、フォーマルエンジンが特定のカバー/シーケンスに一致する最短経路を（理想的に）見つけようとするからです。したがって、多くの実際のシナリオでは、最短経路は正式なエンジンにとって最速ではない可能性があります。これは、正式なエンジンがその特定のカバー状態に達するために多くのフリップフロップをトグルする必要があるかもしれないからである。

私の特定のケースでは、名前「scan_mode」によるフリップフロップは、いくつかの先行するフリップフロップに依存していました。そして、そのため、ツールは 'scan_mode'をアサートするために多くのフリップフロップをフリップする必要がありました。したがって、フリップフロップ（1'b1）上の仮定プロパティは、カバー生成時間を大幅に減少させた。 想定プロパティなしのカバー生成時間：150秒。 想定プロパティによるカバー生成時間：2秒。

Answer 2

トライしたがって「結合」COI

に応じ要する時間は全ての組み合わせがデアサートsignalAをヒットしようとしたことを示し143サイクル未満で実行されます。

全体的に、これらはどれくらい多くの方法で表されますか？&どのくらい速くプロパティがヒットしましたか。