Proof objective function for Stateflow charts and MATLAB Function blocks
sldv.prove( specifies that
expr is true for every evaluation while proving properties.
Use any valid Boolean expression for
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
sldv.prove proof assumptions within the code or
separate the assumptions into a verification script.
Specify Property Proof Objective and Proof Assumption
Specify a property proof objective and proof assumption in
sldvdemo_sqrt_blockrep model by using a MATLAB
sldvdemo_sbr_verification model and save it as
Safety Properties subsystem.
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);
Save the model and return to the top model.
To prove the safety properties, in the Simulink® Editor, select the
subsystem. On the Design Verifier tab, click
Alternatively, in the Simulink Editor, you can right-click the
Properties subsystem and select Design Verifier > Prove Subsystem Properties.
expr — Expression for assumption
Expression for the assumption, specified as a Boolean expression. For
x > 0.
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 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.