Store 
| Products & Services | Solutions | Academia | Support | User Community | Company |
 |
Download Product Updates | | |  |
Get Pricing | | | |
Trial Software |
| Documentation → Simulink Design Verifier |
| Products & Services | Solutions | Academia | Support | User Community | Company |
|
Download Product Updates | | | |
Get Pricing | | | |
Trial Software |
| Documentation → Simulink Design Verifier |
| Contents | Index |
| Learn more about Simulink Design Verifier |
| On this page… |
|---|
In the Design Verifier pane, you specify analysis options and configure Simulink Design Verifier output.
The Design Verifier pane contains the following settings:
This group contains the following controls that enable you to specify how the Simulink Design Verifier software analyzes Simulink models.
Mode. Specifies the mode in which the Simulink Design Verifier software operates— Test generation (the default) or Property proving. Depending on the value of this parameter, if you want to start an analysis, click the Generate Tests or Prove Properties button on this pane.
Maximum analysis time. Specifies the maximum time (in seconds) that the Simulink Design Verifier software spends analyzing the model. The default value is 600 seconds.
Display unsatisfiable test objectives. If you select this option, it causes the Simulink Design Verifier software to display a warning message in the Simulation Diagnostics Viewer when it cannot satisfy a test objective.
Tip If you first select Display unsatisfiable test objectives, set the Test suite optimization option to the Combined objectives strategy and analyze the model. If that test returns objectives without outcomes, select the Individual objectives strategy and reanalyze the model. The Individual objectives strategy analyzes each objective independently and more accurately identifies unsatisfiable objectives. |
Automatic stubbing of unsupported blocks and functions. If you select this option, it specifies that the Simulink Design Verifier software ignores unsupported blocks and functions, and proceeds with the analysis.
This group contains the following controls that enable you to configure Simulink Design Verifier output.
Output directory. Specifies a folder to which the Simulink Design Verifier software writes its output. Enter a path that is either absolute or relative to the current folder.
The default value is sldv_output/$ModelName$. $ModelName$ is a token that represents the model name.
Make output file names unique by adding a suffix. If you select this option, it causes the Simulink Design Verifier software to append an incremental numeric suffix to output file names. Selecting this option prevents the software from overwriting existing files that have the same name.
Click Check Model Compatibility to see if your model is compatible with the Simulink Design Verifier software. If you are setting options for a subsystem that you selected, click Check Subsystem Compatibility.
In the Configuration Parameters dialog box, click Generate Tests or Prove Properties to analyze a model.
If you set the Mode parameter to Test generation, click Generate Tests to begin a test-case generation analysis of the model. If you are setting options for a subsystem that you selected, click Generate Tests for Subsystem.
If you set the Mode parameter to Property proving, click Prove Properties to begin property-proving analysis of the model. If you are setting options for a subsystem that you selected, click Prove Properties of Subsystem.
In the Block Replacements pane, you specify options that control how the Simulink Design Verifier software preprocesses the models it analyzes.
This group contains the following controls that enable you to specify block replacement options.
Apply block replacements. If selected, this option causes the Simulink Design Verifier software to replace blocks in the model before its analysis (see Working with Block Replacements). By default, this option is disabled. Enabling this option provides access to the List of block replacement rules and File path of the output model options.
List of block replacement rules. Specifies a list of block replacement rules that the Simulink Design Verifier software processes before analyzing the model. This option is accessible only if Apply block replacements is selected. The software processes the block replacement rules in the order that you list them.
Specify block replacement rules as a list delimited by spaces, commas, or carriage returns (see Configuring Block Replacements).
The default value is <FactoryDefaultRules>. If you specify the default value, the Simulink Design Verifier software uses its factory default block replacement rules (see Built-In Block Replacements).
File path of the output model. Specifies a folder for the model that results after applying the block replacement rules. Enter a path name that is either absolute or relative to the path name specified as the Output directory. This option is accessible only if Apply block replacements is selected.
The default value is $ModelName$_replacement. $ModelName$ is a token that represents the model name.
In the Parameters pane, you specify options that control how the Simulink Design Verifier software uses parameter configurations when analyzing models.
This group contains the following controls that enable you to specify parameter configurations.
Apply parameters. If selected (the default), this option causes the Simulink Design Verifier software to use parameter configurations when analyzing a model (see Specifying Parameter Configurations). Enabling this option provides access to the Parameter configuration file option.
Parameter configuration file. Specifies an M-file function that defines parameter configurations for a model. Click the Browse button to select an existing M-file function using a file chooser dialog box. Click the Edit button to open the specified M-file function in an editor.
The default value is sldv_params_template.m, a template that you can edit and save. The comments in the template explain the syntax you use to specify parameter configurations.
Tip See the Parameter Identification Example demo for an illustration of how to use parameter configurations when generating tests cases for a Simulink model. |
In the Test Generation pane, you specify options that control how the Simulink Design Verifier software generates tests for the models it analyzes.
This group contains the following controls that enable you to specify test generation options.
Model coverage objectives. Specifies the type of model coverage that the Simulink Design Verifier software attempts to achieve. Select either Decision, Condition Decision, MCDC, or None.
When you set Model coverage objectives to MCDC, the Simulink Design Verifier software automatically enables every coverage objective for decision coverage and condition coverage as well. Similarly, enabling coverage for condition coverage causes every decision and condition coverage outcome to be enabled. Each Simulink Design Verifier coverage objective includes all the objectives in a less-strict coverage metric.
Test conditions. This option allows you to enable or disable Test Condition blocks in the current model either globally or locally. Select one of the following options:
Use local settings — Enables or disables Test Condition blocks based on the value of the Enable parameter of each block. If a block's Enable parameter is selected, the block is enabled; otherwise, the block is disabled.
Enable all — Enables all Test Condition blocks in the model regardless of the settings of their Enable parameters.
Disable all — Disables all Test Condition blocks in the model regardless of the settings of their Enable parameters.
Test objectives. This option allows you to enable or disable Test Objective blocks in the current model either globally or locally. Select one of the following options:
Use local settings — Enables or disables Test Objective blocks based on the value of the Enable parameter of each block. If a block's Enable parameter is selected, the block is enabled; otherwise, the block is disabled.
Enable all — Enables all Test Objective blocks in the model regardless of the settings of their Enable parameters.
Disable all — Disables all Test Objective blocks in the model regardless of the settings of their Enable parameters.
Maximum test case steps. Specifies the maximum number of simulation steps the Simulink Design Verifier software takes when attempting to satisfy a test objective.
Test suite optimization. This option allows you to specify the optimization strategy that the Simulink Design Verifier software uses when generating test cases. Select one of the following options:
Combined objectives — Minimizes the number of test cases in a suite by generating test cases that address more than one test objective. Each test case tends to be long, i.e., it includes many time steps.
This option does not necessarily find unsatisfiable objectives, and often leaves them undecided. To identify unsatisfiable objectives, first, run the Combined objectives strategy to generate test cases. If the analysis returns objectives without outcomes, set the optimization strategy to Individual objectives and rerun the analysis to identify any unsatisfiable objectives.
Individual objectives — Maximizes the number of test cases in a suite by generating test cases that each address only one test objective. Each test case tends to be short, i.e., it includes only a few time steps.
Since each test case is analyzed independently, use this strategy to find unsatisfiable objectives.
Large model — Minimizes the number of test cases in a suite by generating cases that address more than one test objective. This strategy is tailored for large models that contain nonlinearities and numerous test objectives; consequently, it tends to use all the time that the Maximum analysis time option allots.
Long test cases — Combines test cases to create a smaller number of test cases. This strategy generates fewer, but longer, test cases that each satisfy multiple test objectives and creates a more efficient analysis and easier-to-review results.
In the Property Proving pane, you specify options that control how the Simulink Design Verifier software proves properties for the models it analyzes.
This group contains the following controls that enable you to specify property-proving options.
Assertion blocks. This option allows you to enable or disable Assertion blocks in the current model, either globally or locally. Select one of the following options:
Use local settings — Enables or disables Assertion blocks based on the value of the Enable assertion parameter of each block. If a block's Enable assertion parameter is selected, the block is enabled; otherwise, the block is disabled.
Enable all — Enables all Assertion blocks in the model regardless of the settings of their Enable assertion parameters.
Disable all — Disables all Assertion blocks in the model regardless of the settings of their Enable assertion parameters.
Proof assumptions. This option allows you to enable or disable Proof Assumption blocks in the current model either globally or locally. Select one of the following options:
Use local settings — Enables or disables Proof Assumption blocks based on the value of the Enable parameter of each block. If a block's Enable parameter is selected, the block is enabled; otherwise, the block is disabled.
Enable all — Enables all Proof Assumption blocks in the model regardless of the settings of their Enable parameters.
Disable all — Disables all Proof Assumption blocks in the model regardless of the settings of their Enable parameters.
Strategy. Specifies the strategy the Simulink Design Verifier software uses when proving properties. Select one of the following options:
Find violation — If this strategy is selected, the Simulink Design Verifier software searches for property violations within the number of simulation steps specified by the Maximum violation steps option. Enabling this option provides access to the Maximum violation steps option.
Prove — If this strategy is selected, the Simulink Design Verifier software performs property proofs.
Prove with violation detection — This strategy combines the Find violation and Prove strategies. If selected, the Simulink Design Verifier software searches for property violations within the number of simulation steps specified by the Maximum violation steps option; then it attempts to prove properties for which it failed to detect a violation. Enabling this option provides access to the Maximum violation steps option.
See Techniques for Proving Properties of Large Models.
Maximum violation steps. Specifies the maximum number of simulation steps over which the Simulink Design Verifier software searches for property violations. The software does not search beyond the maximum number of simulation steps that you specify; it does not identify violations that occur later in a simulation. This option is accessible only if Strategy specifies either Find violation or Prove with violation detection.
In the Results pane, you specify options that control how the Simulink Design Verifier software handles the results that it generates.
The Results pane contains the following groups of options:
This group contains the following controls that enable you to specify how the Simulink Design Verifier software handles the MAT-file it produces.
Save test data to file. If selected, this option causes the Simulink Design Verifier software to save the test data it generates to a MAT-file. Enabling this option provides access to the Data file name option.
Data file name. Specifies a file name for the MAT-file containing the generated test data. Enter a path name that is either absolute or relative to the folder specified by Output directory. This option is accessible only if Save test data to file is selected.
The default value is $ModelName$_sldvdata. $ModelName$ is a token that represents the model name.
Include expected output values. If selected, this option causes the Simulink Design Verifier software to simulate the model using the test case signals that it produces. For each test case, the software collects the simulation output values associated with Outport blocks in the top-level system and includes those values in the MAT-file that it generates (see TestCases Field / CounterExamples Field).
Randomize data that does not affect outcome. If selected, this option causes the Simulink Design Verifier software to assign random values instead of zeros to test case or counterexample signals that have no impact on test or proof objectives in a model. In the Simulink Design Verifier report, the Generated Input Data table always displays a dash (–) for such signals (see Test Cases / Properties Chapter).
This group contains the following controls that enable you to specify how the Simulink Design Verifier software handles the test harness it produces.
Save test harness as model. If selected, this option causes the Simulink Design Verifier software to save the test harness it generates as a model file. Enabling this option provides access to the Harness model file name option.
Harness model file name. Specifies a file name for the test harness model. Enter a path name that is either absolute or relative to the path name specified by Output directory. This option is accessible only if Save test harness as model is selected.
The default value is $ModelName$_harness. $ModelName$ is a token that represents the model name.
Reference input model in generated harness. If selected, this option causes the Simulink Design Verifier software to use model reference to run the input model in the generated test harness instead of inserting a copy of the input model.
Save test harness as SystemTest TEST-file (will reference saved data file). If selected, this option causes the Simulink Design Verifier software to produce the .test configuration file for running generated test cases inside the SystemTest™ environment. Enter a path name that is either absolute or relative to the path name specified by Output directory. Enabling this option provides access to the SystemTest file name option.
Note The option to create a SystemTest TEST-file is only available in test-generation mode; you cannot create this file when running a property-proving analysis. |
SystemTest file name. Specifies a file name for the SystemTest TEST-file. Enter a path name that is either absolute or relative to the path name specified by Output directory. This option is accessible only if the Save test harness as SystemTest TEST-file (will reference saved data file) is selected.
The default value is $ModelName$_harness. $ModelName$ is a token that represents the model name.
In the Report pane, you specify options that control how the Simulink Design Verifier software reports its results.
This group contains the following controls that enable you to specify report options.
Generate report of the results. If selected, this option causes the Simulink Design Verifier software to save the HTML report it generates. If you select this option, you must also enable the Save test harness as model option (see Harness model options).
Enabling this option provides access to the Report file name, Include screen shots of properties and test objectives, and Display report options.
Report file name. Specifies a file name for the HTML report. Enter a path name that is either absolute or relative to the folder specified by Output directory. This option is accessible only if Generate report of the results is selected.
The default value is $ModelName$_report. $ModelName$ is a token that represents the model name.
Include screen shots of properties and test objectives. If selected, this option causes the Simulink Design Verifier software to insert a screen shot of each property to the corresponding section of the HTML report it generates. This option is only valid in property-proving mode. This option is disabled by default. It is accessible only if Generate report of the results is selected.
Display report. If selected, this option causes the Simulink Design Verifier software to display the HTML report it generates after completing its analysis. This option is enabled by default. It is accessible only if Generate report of the results is selected.
 | Viewing Simulink Design Verifier Options | Saving Simulink Design Verifier Options |  |
Learn more about Simulink through this collection of videos, articles, technical literature and the Getting Started with Simulink Guide.
| © 1984-2009- The MathWorks, Inc. - Site Help - Patents - Trademarks - Privacy Policy - Preventing Piracy - RSS |
