Main Content

sldv.prove

Proof objective function for Stateflow charts and MATLAB Function blocks

collapse all in page

Syntax

sldv.prove(expr)

Description

sldv.prove(expr) specifies that expr is true for every evaluation while proving properties. Use any valid Boolean 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 the code or separate the assumptions into a verification script.

example

Examples

collapse all

Specify a property proof objective and proof assumption in the model sldvdemo_sbr_verification by using a MATLAB Function block.

The command below opens an example in which sldvdemo_sbr_verification model is attached. Open the model.

openExample('sldv/SldvexCCallerBlockExample')

Save sldvdemo_sbr_verification as ex_sldvdemo_sbr_verification.

Open the Safety Properties subsystem.

Open the MATLAB Property block, which is a MATLAB Function block.

At the end of the check_reminder function definition, add sldv.assume(Inputs.KEY==0 | 1); so that the last two lines of the function definition are:

sldv.prove(implies(activeCond, SeatBeltIcon));
sldv.assume(Inputs.KEY==0 | 1);

Save the model and return to the top model.

To prove the safety properties, in the Simulink® Editor, select the Safety Properties subsystem. On the Design Verifier tab, click Prove Properties.

Alternatively, in the Simulink Editor, you can right-click the Safety Properties subsystem and select Design Verifier > Prove Subsystem Properties.

Input Arguments

collapse all

Expression for the assumption, specified as a Boolean expression. For example, x > 0.

Alternatives

Instead of using the sldv.prove function, you can insert a Proof Objective block in your model. To learn about the differences between Proof Objective blocks and sldv.prove, see What Is Property Proving?.

You can also specify a proof objective by using MATLAB for code generation without using the sldv.prove function. Using sldv.prove instead of directly using MATLAB for code generation eliminates the need to:

  • Express the objective by using a Simulink block.

  • Explicitly connect the proof output to a Simulink block.

Version History

Introduced in R2009b

See Also

| | | | |

Topics