Design Verifier Pane: Property Proving

• Property Proving Pane Overview

• Assertion blocks

• Proof assumptions

• Strategy

• Maximum violation steps

Property Proving Pane Overview

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

See Also

• Prove Model Properties Using Simulink Design Verifier

• Workflow for Proving Model Properties

• Prove Properties in a Model

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

• Assertion

• Workflow for Proving Model Properties

• Prove Properties in a Model

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

• Proof Assumption

• Workflow for Proving Model Properties

• Prove Properties in a Model

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 Prove 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

• Prove Model Properties Using Simulink Design Verifier

• Workflow for Proving Model Properties

• Prove Properties in a Model

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

• Prove Model Properties Using Simulink Design Verifier

• Workflow for Proving Model Properties

• Prove Properties in a Model