Main Content

Design Verifier Pane

Configuration parameter window showing Design Verifier pane.

Design Verifier Pane Overview

Specify analysis options and configure Simulink® Design Verifier™ output.

Mode

Specify the analysis mode for Simulink Design Verifier.

Settings

Default: Test generation

Design error detection

Detects integer and fixed-point overflow errors and division-by-zero errors in a model

Test generation

Generates test cases for a model.

Property proving

Proves properties of a model.

Tip

Simulink Design Verifier specifies the value of this option when you select one of these analysis options from the Design Verifier tab, in the Mode section:

  • Select Design Error Detection, then click Detect Design Errors.

  • Select Test Generation, then click Generate Tests.

  • Select Property Proving, then click Prove Properties.

Dependency

When you set the Mode parameter, the button below Check Model Compatibility changes as follows:

  • Mode: Test generation, button reads: Generate Tests

  • Mode: Design error detection, button reads: Detect Errors

  • Mode: Property proving, button reads: Prove Properties

Command-Line Information

Parameter: DVMode
Type: character array
Value: 'TestGeneration' | 'DesignErrorDetection' | 'PropertyProving'
Default: 'TestGeneration'

See Also

Maximum analysis time

Specify the maximum time (in seconds) that Simulink Design Verifier spends analyzing a model. You can set the value of maximum analysis time to the value that you are willing to provide to the analysis. You can also stop the analysis at any time.

Settings

Default: 300

The value that you enter represents the maximum number of seconds Simulink Design Verifier analyzes your model.

Command-Line Information

Parameter: DVMaxProcessTime
Type: double
Value: any valid value
Default: 300

Output folder

Specify a path name to which Simulink Design Verifier writes its output.

Settings

Default: sldv_output/$ModelName$

  • Enter a path that is either absolute or relative to the current folder.

  • $ModelName$ is a token that represents the model name.

  • $CacheFolder$ is a token that represents the Simulink cache folder.

Tip

You can use the following parameters to customize the names and locations of Simulink Design Verifier output:

  • On the Results pane:

    • Data file name

    • Harness model file name

    • Simulink Test options > Test File name

  • On the Report pane:

    • Report file name

    • File path of the output model

  • On the Block Replacements pane:

    • File path of the output model

Command-Line Information

Parameter: DVOutputDir
Type: character array
Value: any valid path
Default: 'sldv_output/$ModelName$'

See Also

Review Analysis Results

Make output file names unique by adding a suffix

Specify whether Simulink Design Verifier makes its output file names unique by appending a numeric suffix.

Settings

Default: On

On

Appends an incremental numeric suffix to Simulink Design Verifier output file names. Selecting this option prevents the software from overwriting existing files that have the same name.

Off

Does not append a suffix to Simulink Design Verifier output file names. In this case, the software might overwrite existing files that have the same name.

Command-Line Information

Parameter: DVMakeOutputFilesUnique
Type: character array
Value: 'on' | 'off'
Default: 'on'

See Also

Review Analysis Results

Check Model Compatibility

Run a check to assess your model for compatibility with Simulink Design Verifier. For more information, see Simulink Design Verifier Checks.

Generate Tests/Detect Errors/Prove Properties

When you set the Mode parameter, this button changes as follows:

Rebuild model representation

Specify whether to rebuild model representation for Simulink Design Verifier analysis.

Settings

Default: If change is detected

Always

Always rebuild the model representation.

If change is detected

Rebuild the model representation only when the software detects any change in the model.

Command-Line Information

Parameter: DVRebuildModelRepresentation
Type: character array
Value: 'Always' | 'IfChangeIsDetected'
Default: 'If change is detected'

See Also

Check Model Compatibility

Automatic stubbing of unsupported blocks and functions

Specify whether to ignore unsupported blocks and functions during analysis.

Settings

Default: On

On

Ignores unsupported blocks and functions and proceeds with the analysis.

Off

Displays a warning when Simulink Design Verifier encounters an unsupported block or function and asks if you want to continue the analysis.

Command-Line Information

Parameter: DVAutomaticStubbing
Type: character array
Value: 'on' | 'off'
Default: 'on'

See Also

Handle Incompatibilities with Automatic Stubbing

Support S-Functions in the analysis

Specify whether to enable support for S-Functions that have been compiled to be compatible with Simulink Design Verifier.

Settings

Default: On

On

Enables support for S-Functions that have been compiled to be compatible with Simulink Design Verifier.

Off

Simulink Design Verifier automatically stubs S-Functions during analysis.

Command-Line Information

Parameter: DVSFcnSupport
Type: character array
Value: 'on' | 'off'
Default: 'on'

See Also

Support Limitations and Considerations for S-Functions and C/C++ Code

Configuring S-Function for Test Case Generation

Handle Incompatibilities with Automatic Stubbing

Use specified input minimum and maximum values

Specify whether to generate test cases that consider specified minimum and maximum values as constraints for all input signals in your model.

Settings

Default: On

On

Considers specified minimum and maximum values as constraints for all input signals.

Off

Ignores any specified minimum and maximum values.

Command-Line Information

Parameter: DVDesignMinMaxConstraints
Type: character array
Value: 'on' | 'off'
Default: 'on'

See Also

Minimum and Maximum Input Constraints

Run additional analysis to reduce instances of rational approximation

Specify whether Simulink Design Verifier attempts to reduce the use of rational approximation during analysis.

Settings

Default: On

On

When you use Simulink Design Verifier to analyze models, Simulink Design Verifier attempts to reduce the use of rational approximation if the model. Enabling this setting may increase analysis time.

Off

Simulink Design Verifier does not attempt to reduce the use of rational approximation during analysis.

Command-Line Information

Parameter: DVReduceRationalApprox
Type: character array
Value: 'on' | 'off'
Default: 'on'

Validate test cases or counterexamples with parallel computing

Specifies whether to validate test cases or counterexamples with parallel computing. This option requires a Parallel Computing Toolbox™ license.

When to Use Parallel Computing for Validation

In general, parallel execution can help reduce the validation time if:

  • You have a complex Simulink model that takes a long time to simulate.

  • The Simulink Design Verifier analysis exceeds the maximum analysis time and results in a number of objectives with the Needs Simulation status. For more information, see Objectives Satisfied - Needs Simulation and Objectives Falsified - Needs Simulation.

  • The test generation analysis generates long test cases. This may be because you have set Test suite optimization to LongTestcases or the Maximum test case steps value is greater than the default value. For more information, see Test Generation Pane Overview.

The following points must be considered when using parallel computing for validation:

  • Starting a parallel pool can take time, which impacts the overall analysis time. To reduce the analysis time:

    • Make sure that the parallel pool is already running before you run a test generation analysis. By default, the parallel pool shuts down after being idle for a specified number of minutes. To change the setting, see the topic 'Specify Your Parallel Preferences' in Parallel Computing Toolbox.

    • Load Simulink on all the parallel pool workers.

  • The simulation occurs sequentially when:

    • The cluster is not local. Configure parallel preferences to use the local cluster only. To change the setting, see the topic 'Specify Your Parallel Preferences' in Parallel Computing Toolbox.

    • The model is in dirty state prior to launching the SLDV analysis.

    • The model has ToFile blocks.

    • The model is an internal harness.

  • Cross-product features such as functional testing and coverage analysis from Simulink Test™ Manager do not support parallel computing for validation. For more information, see Perform Functional Testing and Analyze Test Coverage (Simulink Test).

Settings

Default: Off

On

If you have a Parallel Computing Toolbox license, then Simulink Design Verifier validates test cases or counterexamples in parallel across multiple workers on the same machine.

Off

Simulink Design Verifier validates test cases or counterexamples in serial.

Command-Line Information

Parameter: DVUseParallel
Type: character array
Value: 'on' | 'off'
Default: 'off'

See Also

How Simulink Design Verifier Reports Approximations Through Validation Results

Additional options for code analysis

Specify additional options for analyzing S-functions that have been compiled to be compatible with Simulink Design Verifier. For more information, see Support Limitations and Considerations for S-Functions and C/C++ Code.

Settings

Default: ''

Enter additional options for analyzing S-Functions that have been compiled to be compatible with Simulink Design Verifier. For example, to specify the maximum size of arrays, enter defaultArraySize = 512.

Command-Line Information

Parameter: DVCodeAnalysisExtraOptions
Type: character array
Value: any valid option for analyzing S-Functions
Default: ''

Ignore objectives based on filter

Specify to analyze the model, ignoring the objectives in the Filter file(s). The Filter file(s) contains the model coverage objectives for test generation, dead logic detection, and design error detection objectives that you want to filter from analysis.

Settings

Default: Off

On

Ignores objectives in the Filter file(s) during test generation and design error detection analysis.

Off

Generates results for all the objectives during test generation and design error detection analysis, including those in the Filter file(s).

Dependency

This parameter enables Filter file(s).

Command-Line Information

Parameter: DVCovFilter
Type: character array
Value: 'on' | 'off'
Default: 'off'

See Also

Coverage Filtering (Simulink Coverage)

Filter file(s)

Specify folder and file name(s) for the file(s) that contains the model coverage objectives and design error detection objectives that you want to filter from analysis.

Settings

Default: ''

  • Specify the name of the folder and file name(s) that contain the objectives that you want to ignore from test generation and design error detection analysis.

Click the Filter Explorer button to load an existing Filter file(s) or create a new file.

Command-Line Information

Parameter: DVCovFilterFileName
Type: character array
Value: valid file paths separated by comma or semi-colon
Default: ''

See Also

Coverage Filter Rules and Files (Simulink Coverage)

Filter Objectives by Using Analysis Filter Viewer

Filter Explorer

Click Filter Explorer to load the file(s) that contains objectives that you want to ignore from design error detection and test generation analysis.

Dependency

This button is enabled by Ignore objectives based on filter.