Learn more about Simulink Design Verifier

sldv.assume - Proof assumption

Note dv.assume, which is similar to sldv.assume, will be removed in a future release. Use sldv.assume instead.

Syntax

sldv.assume(expr)

Description

sldv.assume(expr) specifies that expr be true for every evaluation while proving properties. Use any valid Boolean Embedded MATLAB expression for expr.

This function has no output and no impact on its parenting function, other than any indirect side effects of evaluating expr. If you issue this function from the MATLAB command line, the function has no effect.

Intersperse sldv.assume proof assumptions within Embedded MATLAB code or separate the assumptions into a verification script.

The Proof assumptions option in the Property proving pane applies to proof assumptions represented with the sldv.assume function, as well as with the Proof Assumption block.

Examples

Add property proof objective and proof assumption, using Embedded MATLAB expressions.

Open the sldvdemo_sbr_verification model and save it as my_sldvdemo_sbr_verification.
Open the Safety Properties subsystem.
Remove the Assertion block. Instead of the Assertion block, this example uses sldv.prove and sldv.assume.
Open the MATLAB Property Embedded MATLAB Function block.
Delete ok = implies(activeCond,SeatBeltIcon).
To add a proof objective and proof assumption, add these two lines to the check_reminder code.
```
sldv.prove(implies(activeCond,SeatBeltIcon)
sldv.assume(Inputs.KEY==0 | 1)
```
In the Embedded MATLAB editor, save the updated code.
Prove the safety properties: from the Safety Properties subsystem, select Tools > Design Verifier > Prove Properties.

Alternatives

Instead of using the sldv.assume function, you can insert a Proof Assumption block in your model. However, using sldv.assume instead of a Proof Assumption block offers several benefits, described in About Property Proving.

You can also constrain signal values when proving models by using Embedded MATLAB without using the sldv.assume function. However, using sldv.assume instead of directly using Embedded MATLAB eliminates the need to: