Main Content

Design Verifier Pane: Property Proving

Configuration Parameter window showing Property Proving parameter under Design Verifier pane.

Property Proving Pane Overview

Specify options that control how Simulink® Design Verifier™ proves properties for the models it analyzes.

See Also

Assertion blocks

Specify whether Assertion blocks in your model are enabled or disabled.

Settings

Default: Use local settings

Use local settings

Enables or disables Assertion 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 Assertion blocks in the model regardless of the settings of their Enable parameters.

Disable all

Disables all Assertion blocks in the model regardless of the settings of their Enable parameters.

Command-Line Information

Parameter: DVAssertions
Type: character array
Value: 'UseLocalSettings' | 'EnableAll' | 'DisableAll'
Default: 'UseLocalSettings'

See Also

Proof assumptions

Specify whether Proof Assumption blocks in your model are enabled or disabled.

Settings

Default: Use local settings

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.

Command-Line Information

Parameter: DVProofAssumptions
Type: character array
Value: 'UseLocalSettings' | 'EnableAll' | 'DisableAll'
Default: 'UseLocalSettings'

See Also

Strategy

Specify the strategy that Simulink Design Verifier uses when proving properties.

Settings

Default: Prove

Prove

Performs property proofs.

FindViolation

Searches only for property violations within the number of simulation steps specified by the Maximum violation steps option.

ProveWithViolationDetection

Searches both for property violations, as well as tries to prove properties for which it failed to detect a violation. This strategy is a relatively optimal balance between the ProveWithViolationDetection and FindViolation strategies.

Dependency

Selecting FindViolation or ProveWithViolationDetection enables the Maximum violation steps parameter.

Command-Line Information

Parameter: DVProvingStrategy
Type: character array
Value: 'Prove' | 'FindViolation' | 'ProveWithViolationDetection'
Default: 'Prove'

See Also

Maximum violation steps

Specify the maximum number of simulation steps over which Simulink Design Verifier searches for property violations.

Settings

Default: 20

The Simulink Design Verifier software does not search beyond the maximum number of simulation steps that you specify. Therefore, it cannot identify violations that might occur later in a simulation.

Dependency

This parameter is enabled when you set Strategy to FindViolation or ProveWithViolationDetection.

Command-Line Information

Parameter: DVMaxViolationSteps
Type: int32
Value: any valid value
Default: 20

See Also