Use Observer Reference Blocks for Property Proving Analysis

This example uses:

This example shows you how to use an Observer Reference block to perform property proving analysis with multiple properties without making changes to the model. In this example, you replace an existing verification subsystem with an Observer Reference block. However, you can add an Observer Reference block to your model even if your model does not have a verification subsystem to replace. For more information, see Access Model Data Wirelessly by Using Observers (Simulink Test).

The model sldvdemo_debounce_validprop is configured for analysis and attempts to prove that:

When the current and six previous input values are true, the output will be true.
When the current and six previous input values are false, the output will be false.

For a detailed description of the Observer Reference block, see Isolate Verification Logic with Observers.

Step 1: Open the Model

The sldvdemo_debounce_validprop model contains a verification subsystem called Verify Output. For more information on the Verification Subsystem, see Verification Subsystem. To open the model, enter:

open_system('sldvdemo_debounce_validprop');

Step 2: Replace the Verification Subsystem with an Observer Reference Block

Perform these steps to create a new Observer Reference block and replace the Verify Output verification subsystem.

1. Right-click the Verify Output subsystem. In the context menu, click Observers > Move selected block to Observer > New Observer.

2. Click Yes in the dialog box that appears.

3. An Observer Reference block replaces the verification subsystem. The sldvdemo_debounce_validprop_Observer1 Observer model opens.

4. Save sldvdemo_debounce_validprop_Observer1 in a writable folder on the MATLAB path.

5. Double-click one of the Observer Port blocks to open the Manage Observer Block window. The two signals, debounce and raw, are automatically map to the two Observer Port blocks in the sldvdemo_debounce_validprop_Observer1 Observer model.

Step 3: Perform Property Proving Analysis

To perform the property proving analysis, follow these steps:

1. In the top-level model, on the Design Verifier tab, click Prove Properties.

2. After the analysis completes, the Simulink Design Verifier Results Summary window reports that two objectives are satisfied.

3. Open the HTML analysis report to see a detailed report that includes information about the top-level model and Observers.

Step 4: Review the Property Proving Analysis Report

The analysis report shows the Observer information for property proving in the Observer Model(s) section of the Properties chapter..

Step 5: Cleanup

Close the model.

bdclose('sldvdemo_debounce_validprop');