Main Content

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

Design Verifier ペイン

Design Verifier ペインの概要

解析オプションの指定および Simulink® Design Verifier™ 出力の構成を行います。

モード

Simulink Design Verifier の解析モードを指定します。

設定

既定の設定: テスト生成

設計エラー検出

モデルの整数および固定小数点のオーバーフロー エラー、およびゼロ除算エラーを検出します。

テスト生成

モデルのテスト ケースを生成します。

プロパティ証明

モデルのプロパティを証明します。

ヒント

Simulink Design Verifier は、[Design Verifier] タブの [モード] セクションで以下のいずれかの解析オプションを選択したとき、そのオプションの値を指定します。

  • [設計エラー検出] を選択し、[設計エラーの検出] をクリックします。

  • [テスト生成] を選択し、[テストの生成] をクリックします。

  • [プロパティ証明] を選択し、[プロパティの証明] をクリックします。

依存関係

[モード] パラメーターの設定により、[モデルの互換性のチェック] の下のボタンは次のように変化します。

  • モード: テスト生成 の場合、ボタン: テストの生成

  • モード: 設計エラー検出の場合、ボタン: エラーの検出

  • モード: プロパティ証明 の場合、ボタン: プロパティの証明

コマンド ライン情報

パラメーター: DVMode
タイプ: 文字配列
値: 'TestGeneration' | 'DesignErrorDetection' | 'PropertyProving'
既定の設定: 'TestGeneration'

参考

最大解析時間

Simulink Design Verifier がモデルの解析に費やす最大時間を秒単位で指定します。最大解析時間の値は、解析に指定しても構わない値に設定できます。また、解析はいつでも停止できます。

設定

既定の設定: 300

入力された値は、Simulink Design Verifier がモデルの解析に費やす最大秒数を表します。

コマンド ライン情報

パラメーター: DVMaxProcessTime
タイプ: double
値: 任意の有効な値
既定の設定: 300

出力フォルダー

Simulink Design Verifier による出力の書き込み先のパス名を指定します。

設定

既定の設定: sldv_output/$ModelName$

  • 現在のフォルダーの絶対パスまたは相対パスを入力します。

  • $ModelName$ は、モデル名を表すトークンです。

ヒント

次のパラメーターを使用して、Simulink Design Verifier の出力の名前および場所をカスタマイズできます。

  • [結果] ペイン:

    • データ ファイル名

    • ハーネス モデルのファイル名

    • [Simulink テスト オプション]、[テスト ファイル名]

  • [レポート] ペイン:

    • レポート ファイル名

    • 出力モデルのファイル パス

  • [ブロック置換] ペイン:

    • 出力モデルのファイル パス

コマンド ライン情報

パラメーター: DVOutputDir
タイプ: 文字配列
値: 任意の有効なパス
既定の設定: 'sldv_output/$ModelName$'

参考

解析結果のレビュー

接尾辞を追加して出力ファイル名を固有にする

Simulink Design Verifier が数値の接尾辞を追加して出力ファイル名を一意にするかどうかを指定します。

設定

既定の設定: オン

オン

数字をインクリメントする接尾辞を Simulink Design Verifier 出力ファイル名に追加します。このオプションを選択することで、同名の既存のファイルが上書きされないようにします。

オフ

接尾辞を Simulink Design Verifier 出力ファイル名に追加しません。この場合、このソフトウェアは同名の既存のファイルを上書きする可能性があります。

コマンド ライン情報

パラメーター: DVMakeOutputFilesUnique
タイプ: 文字配列
値: 'on' | 'off'
既定の設定: 'on'

参考

解析結果のレビュー

モデルの互換性チェック

チェックを実行してモデルと Simulink Design Verifier の互換性を評価します。詳細は、Simulink Design Verifier のチェックを参照してください。

テストの生成/エラーの検出/プロパティの証明

[モード] パラメーターを設定すると、このボタンは次のように変化します。

  • モード: テスト生成 の場合、ボタン: テストの生成

    詳細については、テスト ケースの生成とはを参照してください。

  • モード: 設計エラー検出の場合、ボタン: エラーの検出

    詳細については、設計エラー検出とはを参照してください。

  • モード: プロパティ証明 の場合、ボタン: プロパティの証明

    詳細については、プロパティ証明とはを参照してください。

モデル表現の再作成

モデル表現を Simulink Design Verifier 解析用に再作成するかどうかを指定します。

設定

既定の設定: 変更が検出された場合

常時

モデル表現を常に再作成します。

変更が検出された場合

モデルの変更が検出されたときにのみ、モデル表現を再作成します。

コマンド ライン情報

パラメーター: DVRebuildModelRepresentation
タイプ: character array
値: 'Always' | 'IfChangeIsDetected'
既定の設定: 'If change is detected'

参考

モデルの互換性チェック

未サポートのブロックおよび関数の自動スタブ化

サポートされていないブロックと関数を解析時に無視するかどうかを指定します。

設定

既定の設定: オン

オン

サポートされないブロックおよび関数を無視して、解析を続行します。

オフ

Simulink Design Verifier がサポートされないブロックまたは関数を検出した場合、警告を表示し、解析を続行するかどうかを尋ねます。

コマンド ライン情報

パラメーター: DVAutomaticStubbing
タイプ: 文字配列
値: 'on' | 'off'
既定の設定: 'on'

参考

自動スタブによる非互換性処理

解析で S-Function をサポート

Simulink Design Verifier との互換性をもつようにコンパイルされた S-Function のサポートを有効にするかどうかを指定します。

設定

既定の設定: オン

オン

Simulink Design Verifier との互換性をもつようにコンパイルされた S-Function のサポートを有効にします。

オフ

Simulink Design Verifier は解析時に自動的に S-Function をスタブします。

コマンド ライン情報

パラメーター: DVSFcnSupport
タイプ: 文字配列
値: 'on' | 'off'
既定の設定: 'on'

参考

S-Function および C/C++ コードのサポートの制限事項と考慮事項

テスト ケース生成のための S-Function の構成

自動スタブによる非互換性処理

指定された最小/最大入力値の使用

指定された最小値および最大値を、モデル内のすべての入力信号に対する制約として考慮するテスト ケースを生成するかどうかを指定します。

設定

既定の設定: オン

オン

指定された最小値および最大値をすべての入力信号への制約として考慮します。

オフ

指定された最小値および最大値を無視します。

コマンド ライン情報

パラメーター: DVDesignMinMaxConstraints
タイプ: 文字配列
値: 'on' | 'off'
既定の設定: 'on'

参考

最小値と最大値の入力制約

有理近似のインスタンスを減らすために追加の解析を実行

Simulink Design Verifier が解析時に有理近似の使用を減らそうとするかどうかを指定します。

設定

既定の設定: オン

オン

Simulink Design Verifier を使用してモデルを解析する際に、Simulink Design Verifier はモデル内での有理近似の使用を減らそうとします。この設定を有効にすると、解析時間が長くなる場合があります。

オフ

Simulink Design Verifier は解析時に有理近似の使用を減らしません。

コマンド ライン情報

パラメーター: DVReduceRationalApprox
タイプ: 文字配列
値: 'on' | 'off'
既定の設定: 'on'

並列計算でテスト ケースまたは反例を検証

並列計算でテスト ケースまたは反例を検証するかどうかを指定します。このオプションには Parallel Computing Toolbox™ のライセンスが必要です。

検証で並列計算を使用する場合

一般に、次の場合に、並列実行で検証時間を削減できます。

検証に並列計算を使用する場合は、次の点を考慮しなければなりません。

  • 並列プールを起動するには時間がかかり、解析時間全体に影響します。解析時間を削減するには、次のようにします。

    • テスト生成解析を実行する前に、並列プールが既に実行されていることを確認します。既定の設定では、指定した分単位の値にわたりアイドル状態になると、並列プールはシャットダウンします。この設定を変更する場合は、Parallel Computing Toolbox のトピック「並列基本設定の指定」を参照してください。

    • すべての並列プール ワーカーで Simulink を読み込みます。

  • 次の場合、シミュレーションは順次行われます。

    • クラスターは local ではない。local クラスターのみを使用するように、並列基本設定を構成します。この設定を変更する場合は、Parallel Computing Toolbox のトピック「並列基本設定の指定」を参照してください。

    • SLDV 解析を起動する前のモデルは dirty state である。

    • モデルに ToFile ブロックがある。

    • このモデルは内部ハーネスです。

  • Simulink Test™ マネージャーからの機能テストとカバレッジ解析などの製品間の機能では、検証の並列計算をサポートしていません。詳細については、機能テストの実行とテスト カバレッジの解析 (Simulink Test)を参照してください。

設定

既定の設定: オフ

オン

Parallel Computing Toolbox ライセンスがある場合、Simulink Design Verifier は同じマシンの複数のワーカーにわたって、テスト ケースまたは反例を並列で検証します。

オフ

Simulink Design Verifier はテスト ケースまたは反例を逐次検証します。

コマンド ライン情報

パラメーター: DVUseParallel
タイプ: 文字配列
値: 'on' | 'off'
既定の設定: 'off'

参考

Simulink Design Verifier が検証結果を使用して近似をレポートする方法

コード解析の追加オプション

Simulink Design Verifier との互換性をもつようにコンパイルされた S-Function を解析するための追加オプションを指定します。詳細については、S-Function および C/C++ コードのサポートの制限事項と考慮事項を参照してください。

設定

既定の設定: ''

Simulink Design Verifier との互換性をもつようにコンパイルされた S-Function を解析するための追加オプションを入力します。たとえば、配列の最大サイズを指定するには、「defaultArraySize = 512」と入力します。

コマンド ライン情報

パラメーター: DVCodeAnalysisExtraOptions
タイプ: 文字配列
値: S-Function の解析に有効な任意のオプション
既定の設定: ''

フィルターを基にオブジェクティブを無視する

[フィルター ファイル] のオブジェクティブを無視して、モデルを解析することを指定します。[フィルター ファイル] には、解析から除外するテスト生成用のモデル カバレッジ オブジェクティブ、デッド ロジック検出オブジェクティブ、および設計エラー検出オブジェクティブが含まれます。

設定

既定の設定: オフ

オン

テスト生成および設計エラー検出解析中に、[フィルター ファイル] に含まれるオブジェクティブを無視します。

オフ

[フィルター ファイル] に含まれるものも含め、テスト生成および設計エラー検出解析時にすべてのオブジェクティブについて結果を生成します。

依存関係

このパラメーターは [フィルター ファイル] を有効にします。

コマンド ライン情報

パラメーター: DVCovFilter
タイプ: 文字配列
値: 'on' | 'off'
既定の設定: 'off'

参考

カバレッジのフィルター (Simulink Coverage)

フィルター ファイル

解析から除外するモデル カバレッジ オブジェクティブおよび設計エラー検出オブジェクティブを含むファイルのフォルダー名とファイル名を指定します。

設定

既定の設定: ''

  • テスト生成および設計エラー検出解析で無視するオブジェクティブを含むフォルダー名とファイル名を指定します。

[フィルター エクスプローラー] ボタンをクリックして、既存の [フィルター ファイル] を読み込むか新しいファイルを作成します。

コマンド ライン情報

パラメーター: DVCovFilterFileName
タイプ: 文字配列
値: コンマまたはセミコロンで区切った有効なファイル パス
既定の設定: ''

参考

カバレッジ フィルターの規則とファイル (Simulink Coverage)

[解析フィルター] ビューアーを使用したオブジェクティブのフィルター処理

フィルター エクスプローラー

[フィルター エクスプローラー] をクリックして、設計エラー検出およびテスト生成解析で無視するオブジェクティブを含むファイルを読み込みます。

依存関係

このボタンは、[フィルターを基にオブジェクティブを無視する] によって有効になります。