問題タブ [formal-verification]

大きな設計で小さなモジュールを正式に検証しています。

設計を分析し、精緻化しました (Jaspergold -fpv を使用)。

非常に単純なカバー プロパティ (SVA) を次のように記述しました。

カバーを見つけるのに約 5300 秒かかります。"Bound" が 143 であることに気付きました。

では、なぜカバーを生成するのにこれほど時間がかかるのでしょうか? また、これは何を意味するのでしょうか (時間と拘束時間)?

ツールがカバーを生成するために設計状態を深く調べる必要があり、COI が大きいためでしょうか? それとも他の理由？

ご協力いただきありがとうございます。

システムとその完全な状態空間が与えられた場合、その状態空間はそのシステムの動作の正式な仕様であると言えますか?

ここで問題をより明確に変更しました。送信側モデルと受信側モデルの 2 つの異なるモデルがあります。送信されたメッセージが受信者が受信したものと同じではないというプロパティを確認したい。

LTLSPEC (G(状態=受信者 -> messageTransmited != messageReceived))

私はアサーション ベースの検証の初心者であり、それが適切に行われる方法を学ぼうとしています。systemverilog + assertions に関する構造と技術的な詳細に関する多くの情報を見つけましたが、現実の世界で物事が実際にどのように行われるかについてのある種の「クックブック」資料をまだ見つけていません。

質問と制約:

• デザインには、 data、valid、およびid入力を含むデータ入力バスがあります。
• 1データ「パッケージ」は3サンプル
• チャネルnの後には、チャネルn+1からのデータが常に存在します。
  • チャネル ID は、最大の ID が送信された後にラップされます
• データ バイト間に任意の数の clk ティックを含めることができます

• 以下は、チャネル ID を使用した単純でうまくいけば正しいタイミング図です。

  

では、最小限のコードでこれを行うにはどうすればよいでしょうか。素敵できれい。以前は、データを駆動するダミーの Verilog モジュールを作成しました。しかし、仮定プロパティを使用してチャネル ID を制約することはできますが、それ以外の場合は、正式なツールが私の設計にブレーキをかけようとする自由な手は残しておいてください。

スターター向けのシンプルなテンプレートは次のとおりです。

問題は、上記のような仮定/アサーションがすべてのデータサンプルでトリガーされ、時間的に重複する並列スレッドを作成する傾向があることだと思います。

次のポーズエッジが完了してから 4 サイクル後に req が高くなるというアサーションを書きたいと思います。私にとって、リセット時の完了はすでに高いです。完了の次のポーズエッジでリクエストを高くするにはどうすればよいですか。assert property {$rose(done) |-> ##4 req}しかし、なぜそれが機能しないのかわかりません。誰でも助けてもらえますか？

合金初心者です。

私は、Alloy で制約を作成し、モデルが制約に従って有効であることをアナライザーにチェックさせるのが本当に好きです。

しかし、「これらの制約の定義は単なる頭の体操ですか? それとも、より良いソフトウェアの構築に役立つでしょうか?」</p>

具体例を挙げてみましょう。電子メール クライアントのアドレス帳のモデルでは、アドレス帳に新しいエントリを追加するために次の制約を定義できます。

新しいブック b' のアドレス マッピングは、古いブック b のアドレス マッピングと同じですが、名前からアドレスへのリンクが追加されています。この制約は Alloy では次のように表されます: b'.addr = b.addr + n->a

それは美しいです。

しかし、追加操作がコードに実装されている場合、その関連性を確認するのに苦労しています。たとえば、Common Lisp でadd操作を実装しました。

つまり、「これはaddという名前の関数の定義で、3 つのパラメーターb、n、およびa (本、名前、住所) を持ちます。Common Lisp の set 関数adjoinを使用して、リスト ( na ) をbに追加します。"</p>

その関数は、単純な追加関数を正しく実装しているようです。Alloy で定義した拘束はどうすればよいですか? 制約を表現する追加のコードを作成する必要がありますか? 擬似コード: [1]

このようなコードを書くのは大変な作業のように思えますが、明らかなメリットはありません。

私の質問は次のとおりです: コードで Alloy モデルを実装する場合、Alloy で定義されている制約をどうすればよいですか?

また、Alloy モデルをコードに変換する方法を説明するチュートリアルはありますか? コードで Alloy 制約定義がどのように使用されるかの説明が含まれていますか?

ありがとうございました。

[1] 注: Common Lisp には Screamer という制約プログラミング用の言語拡張があることを認識しています。

これら2つのステートメントが等しいことをどのように証明できますか:

1. Val.shru (Val.and a (Vint b)) (Vint c) = Vint ?3434 /\ ?3434 <> d

2. Val.shru (Val.and a (Vint b)) (Vint c) <> d

コンセプトは非常にシンプルですが、それを解決するための適切な戦術を見つけることに行き詰まっています。これは実際に私が証明しようとしている Lemma です:

ありがとう、