Learn more about Simulink Design Verifier

sldv.prove - Proof objective

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

Syntax

sldv.prove(expr)

Description

sldv.prove(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.prove proof assumptions within Embedded MATLAB code or separate the assumptions into a verification script.

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.prove function, you can insert a Proof Objective block in your model.

However, using sldv.prove instead of a Proof Objective block offers several benefits, described in About Property Proving.

You can also specify a proof objective by using Embedded MATLAB without using the sldv.prove function. However, using sldv.prove instead of directly using Embedded MATLAB eliminates the need to: