Main Content

Proof Assumption

Constrain signal values when proving model properties

expand all in page
  • Proof Assumption block

Libraries:
Simulink Design Verifier / Objectives and Constraints

Description

When operating in property-proving mode, the Simulink® Design Verifier™ software proves that properties of your model satisfy specified criteria (see What Is Property Proving?). In this mode, you can use Proof Assumption blocks to define assumptions for signals in your model. The Values parameter lets you specify constraints on signal values during a property proof. The block applies the specified Values parameter to its input signal, and the Simulink Design Verifier software proves or disproves that the properties of your model satisfy the specified criteria.

The block's parameter dialog box also allows you to:

  • Enable or disable the assumption.

  • Specify that the block should display its Values parameter in the Simulink Editor.

  • Specify that the block should display its output port.

Note

The Simulink and Simulink Coder™ software ignore the Proof Assumption block during model simulation and code generation, respectively. The Simulink Design Verifier software uses the Proof Assumption block only when proving model properties.

You can constrain signal values in property proofs by using Values parameters. For more information, see Set Parameters Using Parameter Configuration File.

Examples

Property Proving with an Assumption Block

Property Proving with an Assumption Block

Perform a Simulink® Design Verifier™ property proof using a Proof Assumption block. It attempts to prove that when the sum of the current and six previous input values is greater than 6, the output equals 2. The model includes a Proof Assumption block that constrains the input to be 0 or 1. Simulink Design Verifier searches for violations of 20 or fewer time steps. It is unable to find a violation because the property is valid under the assumption.

Ports

Input

expand all

The Proof Assumption block accepts signals of all built-in data types supported by the Simulink software. For a discussion on the data types supported by the Simulink software, see Data Types Supported by Simulink. The block does not support complex input signals.

Data Types: single | double | int8 | int16 | int32 | int64 | uint8 | uint16 | uint32 | uint64 | Boolean | fixed point | enumerated | bus

Output

expand all

The Proof Assumption block returns signals of all built-in data types supported by the Simulink software. For more information about supported data types, see Data Types Supported by Simulink.

Data Types: single | double | int8 | int16 | int32 | int64 | uint8 | uint16 | uint32 | uint64 | Boolean | fixed point | enumerated | bus

Parameters

expand all

Specify whether the block is enabled. If selected (the default), the Simulink Design Verifier software uses the block when proving properties of a model. Clearing this option disables the block, that is, causes the Simulink Design Verifier software to behave as if the Proof Assumption block did not exist. If this option is not selected, the block appears grayed out in the Simulink Editor.

Specify whether the block behaves as a Proof Assumption or Test Condition block. Select Test Condition to transform the Proof Assumption block into a Test Condition block.

Use the Values parameter to constrain signal values in test cases. Specify any combination of scalars and intervals in the form of a MATLAB® cell array. For more information, see Set Parameters Using Parameter Configuration File.

Specify whether the block displays the contents of its Values parameter in the Simulink Editor.

If selected, the block displays its output port, which allows the input signal to pass through to the block output. If not selected, the block hides its output port and terminates the input signal.

Example: The following graphics illustrate the appearance of the block in each case.

Pass through style (show Outport): Selected

Pass through style (show Outport): Deselected

Version History

Introduced in R2007a

See Also

|