Main Content

What Is Property Proving?

A property is a requirement that you model in Simulink® or Stateflow®, or by using MATLAB Function or Requirements Table blocks. A property can be a simple requirement, such as a signal in your model that must attain a particular value or range of values during simulation.

A property can also be a requirement on the model that involves a number of input and output signals modeled as a logical expression that needs to be proved.

The Simulink Design Verifier™ software performs a formal analysis of your model to prove or disprove the specified properties. After completing the analysis, the software offers several ways for you to review the results:

  • Highlighted on the model

  • A harness model with test cases

  • A detailed HTML report

Proof Blocks

The Simulink Design Verifier software provides two blocks so you can specify property proofs in your Simulink models:

Note

Blocks from the Model Verification library in the Simulink software behave like Proof Objective blocks during Simulink Design Verifier proofs. You can use Assertion blocks and other Model Verification blocks to specify properties of your model. For more information about these blocks, see Model Verification.

Proof Functions

The Simulink Design Verifier software provides two Stateflow and MATLAB® for code generation functions to specify property proving for a Simulink model or Stateflow chart:

These functions:

  • Identify mathematical relationships for proving properties in a form that can be more natural than using block parameters

  • Support specifying multiple objectives, assumptions, or conditions without complicating the model.

  • Provide access to the power of MATLAB.

  • Support separation of verification and model design.

For an example of how to use these proof functions, see the sldv.prove reference page.

Note

Simulink Design Verifier blocks and functions are saved with a model. If you open the model on a MATLAB installation that does not have a Simulink Design Verifier license, you can see the blocks and functions, but they do not produce results.