このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

Assumption ブロックによるプロパティ証明

この例では、Proof Assumption ブロックを使用した、Simulink® Design Verifier™ のプロパティ証明の実行方法を示します。これは、現在の入力値および以前の 6 つの入力値の合計が 6 より大きい場合、出力が 2 と等しいことを証明しようとします。モデルには入力を 0 または 1 に制約する Proof Assumption ブロックが含まれます。Simulink Design Verifier は 20 以下のタイム ステップの違反を検索します。仮定に基づいてプロパティが有効であるため、違反を見つけることはできません。

open_system('sldvdemo_debounce_assumeblk');