問題タブ [formal-verification]

私は Dafny を使用して、あなたが受け取る削除メソッドを作成しています:

• 文字配列line

• 配列の長さl

• 位置at

• 削除する文字数p

最初に at から to までの行の文字を削除し、次にtoat + pの右側のすべての文字を移動する必要があります。at + pat

たとえば、[e][s][p][e][r][m][a]、 、at = 3、およびp = 3がある場合、最終結果は次のようになります。[e][s][p][a]

私は次のような意味のある事後条件を証明しようとしています:

ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]);

at + p の右側からのすべての文字が新しい位置にあることを確認します。

しかし、Dafny は 2 つのエラーを出力します。

範囲外のインデックス 7 53

このリターン パスでは事後条件が保持されない可能性があります。19 2

rise4funのプログラムはこちら

ダフニーを通過させるために、以下に何を追加する必要があるのだろうか？

検索、削除、および挿入メソッドを使用する検索および置換メソッドをコーディングしています。while ループ内でこれら 3 つのメソッドを呼び出していますが、どの前提条件を使用すればよいかわかりません。

完全なコード:

動作を正式に検証するために、SVA にプロパティを記述したいと考えています。

これが私がしたいことです：

sig1 が落ちた後、残りの評価サイクル中に LOW のままになるように、上記のプロパティを書き換えるにはどうすればよいですか?

注: sig1 をディセーブル iff (sig1) として配置したくありません。

3 つの正式な検証ツールを比較するために考慮すべき要素は何ですか? 例: Jaspergold、Onespin、Incisive。

私のちょっとした調査によると、Jaspergold が一番です。しかし、私はプロジェクトで自分でやりたいです。

1. サポートされている言語 (vhdl、sv、verilog、sva、psl など) 2. GUI 3. 機能 (どれだけ大きなデザインを処理できるか) 4. 評価サイクルの数 5. パフォーマンス (証明や反例を見つける速度）

このリストを拡張できる他の機能は何ですか?

ありがとう！

更新しました

特定のクラスとそれぞれのメソッドを使用して以下に説明する、いくつかのダフニーの問​​題を解決する際の問題。他に何か必要な場合は、教えてください。事前に感謝します。また、rise4fun のこのすべてのコードでリンクが更新されます。

オンライズ4ファン

I am wondering if there is an operator for Records in z3 similar to the "store" operator for arrays. That is, given a record, is there any way to return a new record in which we've changed one element and all other elements retain their values? For instance:

The last line above is an example of what I would like to do. Is there any way to do this? Or is the user-defined constructor the only means to construct a new record? Thank you.

アーキテクチャ内で次のように機能します。

この関数が期待どおりに動作することを確認したいと思います。だから私は私のSVAファイルに同様の（正確ではない）関数を書きました。

しかし、エラーが発生します:「外部参照関数は未解決のままです」

アサーション ファイルに外部参照を追加するにはどうすればよいですか?

iff sig1=1'b1最初のクロック サイクルの後にプロパティを無効にしたい。

ハイからローへの移行sig1が私のトリガー条件です。私が行うと、disable iff(sig1)トリガー条件が満たされなくなります。

またthroughout、正式な検証者の有効化シーケンスと満足シーケンスの両方で使用することはできません。

どうすればできますか？ありがとう！