Proof assumption function for Stateflow charts and MATLAB Function blocks
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
sldv.assume proof assumptions
within MATLAB code or separate the assumptions into a verification
The Proof assumptions option in the Property proving
pane applies to the proof assumptions represented by the
function and by the Proof Assumption block.
Specify Property Proof Objective and Proof Assumption
Specify a property proof objective and proof assumption in
sldvdemo_sbr_verification model by using a MATLAB
sldvdemo_sbr_verification model and save it as
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,
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);
To save the updated code, in the Editor tab, click Save and close the editor.
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.
expr — Boolean expression for assumption
MATLAB expression, for example,
x > 0.
Instead of using the
sldv.assume function, you can insert a Proof
Assumption block in your model. Using
of a Proof Assumption block offers several benefits, described in What Is Property Proving?.
When proving models by using MATLAB for code generation, you can also constrain signal values without using
sldv.assume function. Using
instead of directly using MATLAB for code generation eliminates the need to:
Express the assumption by using a Simulink block.
Explicitly connect the assumption output to a Simulink block.