Highlight Results on the Model

Results Review with Model Highlighting

When you analyze a model by using Simulink^® Design Verifier™, the analyzed model objects are automatically highlighted in one of these colors:

Green
Red
Orange
Gray

You can review the analysis results at a glance by viewing the objects that are highlighted in the Simulink Editor.

Simulink Design Verifier Results Inspector

When a model is highlighted, you can click an object for which the analysis recorded results. The Simulink Design Verifier Results Inspector then displays the detailed analysis results for that object.

Highlight Results on Model Automatically

During analysis, Simulink Design Verifier highlights the model objects automatically when the objectives status is updated. By default, the automatic highlighting is enabled. To disable the highlighting, click Disable Highlighting in the Results Summary window.

In the Simulink Editor, results highlighting appears on the model. When highlighting is enabled, the Results Inspector opens displaying the summary of status for analysis objectives.

Note

Simulink Design Verifier does not highlight the Stateflow^® state transition tables. The Simulink Design Verifier reports, data files, and log files include the analysis data for the state transition tables. Using the report, you can navigate to the state transition tables.

Green Highlighting on Model

Objects that are highlighted in green have the following meaning for each type of analysis.

Analysis Mode	Green highlighting
Design error detection	The analysis did not find overflow or division-by-zero errors. The analysis did not find dead logic. The analysis did not find intermediate or output signals outside the range of user-specified minimum and maximum constraints. The analysis did not find out of bound array access errors.
Test generation	The analysis found test cases that satisfy the test objectives.
Property proving	The analysis found all the proof objectives as valid.

Red Highlighting on Model

Objects that are highlighted in red have the following meaning, depending on the analysis type.

Analysis Mode	Red highlighting
Design error detection	The analysis found at least one test case that causes overflow or division-by-zero errors. The analysis found dead logic. The analysis found intermediate or output signals outside the range of user-specified minimum and maximum constraints. The analysis found at least one test case that causes an out of bound array access error.
Test generation	The analysis did not satisfy certain test objectives.
Property proving	The analysis disproved a proof objective and generated a counterexample that falsified that objective.

If your model contains at least one object highlighted in red, there might be further design errors in your model that Simulink Design Verifier does not highlight in red. If an object in your design causes run-time errors, Simulink Design Verifier might not be able to determine further errors on objects that are downstream of or rely on the results of the object that causes the run-time errors. Resolve the errors that cause the initial red highlighting and rerun the analysis to determine if Simulink Design Verifier highlights other objects in your model as red.

Orange Highlighting on Model

Objects that are highlighted in orange have the following meaning, depending on the analysis type.

Analysis Mode	Orange highlighting
Design error detection	For the highlighted model object, The analysis did not decide at least one design error detection objective. This situation can occur when: The analysis is still in progress. The analysis times out. The analysis cannot decide a design error detection objective because of division by zero or nonlinear arithmetic. The software cannot decide a design error detection objective because of stubbing. For more information, see Handle Incompatibilities with Automatic Stubbing. The software cannot decide a design error detection objective because of limitations of the analysis engine. For example, if the analysis encounters an unbounded while loop, it performs an approximation. For more information, see Role of Approximations During Model Analysis. The analysis found dead logic that approximations can impact. For more information, see How Simulink Design Verifier Reports Approximations Through Validation Results. The analysis found valid objectives that approximations can impact. For more information, see How Simulink Design Verifier Reports Approximations Through Validation Results.
Test generation	For the highlighted model object, The analysis did not decide at least one test objective. This situation can occur when: The analysis is still in progress. The analysis times out. The analysis cannot decide a test objective because of division by zero or nonlinear arithmetic. The software cannot decide a test objective because of stubbing. For more information, see Handle Incompatibilities with Automatic Stubbing. The software cannot decide a test objective because of limitations of the analysis engine. For example, if the analysis encounters an unbounded while loop, it performs an approximation. For more information, see Role of Approximations During Model Analysis. The analysis found unsatisfiable objectives that approximations can impact. For more information, see How Simulink Design Verifier Reports Approximations Through Validation Results. The analysis is unable to confirm the satisfied status through validation results. For more information, see Objectives Satisfied - Needs Simulation.
Property proving	For the highlighted model object, The analysis did not decide at least one proof objective. This situation can occur when: The analysis is still in progress. The analysis times out. A proof objective exists on a signal whose value the software cannot control, for example, a Constant block. The analysis cannot decide a proof objective because of division by zero or nonlinear arithmetic. The software cannot decide a proof objective because of stubbing. For more information, see Handle Incompatibilities with Automatic Stubbing. The software cannot decide a proof objective because of limitations of the analysis engine. For example, if the analysis encounters an unbounded while loop, it performs an approximation. For more information, see Role of Approximations During Model Analysis. The analysis found valid objectives that approximations can impact. For more information, see How Simulink Design Verifier Reports Approximations Through Validation Results. The software is unable to confirm the falsified status through validation results. For more information, see Objectives Falsified - Needs Simulation.

Analysis Mode

Orange highlighting

Design error detection

For the highlighted model object,

The analysis did not decide at least one design error detection objective. This situation can occur when:
- The analysis is still in progress.
- The analysis times out.
- The analysis cannot decide a design error detection objective because of division by zero or nonlinear arithmetic.
- The software cannot decide a design error detection objective because of stubbing. For more information, see Handle Incompatibilities with Automatic Stubbing.
- The software cannot decide a design error detection objective because of limitations of the analysis engine. For example, if the analysis encounters an unbounded while loop, it performs an approximation. For more information, see Role of Approximations During Model Analysis.

The analysis found dead logic that approximations can impact. For more information, see How Simulink Design Verifier Reports Approximations Through Validation Results.
The analysis found valid objectives that approximations can impact. For more information, see How Simulink Design Verifier Reports Approximations Through Validation Results.

Test generation

For the highlighted model object,

The analysis did not decide at least one test objective. This situation can occur when:
- The analysis is still in progress.
- The analysis times out.
- The analysis cannot decide a test objective because of division by zero or nonlinear arithmetic.
- The software cannot decide a test objective because of stubbing. For more information, see Handle Incompatibilities with Automatic Stubbing.
- The software cannot decide a test objective because of limitations of the analysis engine. For example, if the analysis encounters an unbounded while loop, it performs an approximation. For more information, see Role of Approximations During Model Analysis.

The analysis found unsatisfiable objectives that approximations can impact. For more information, see How Simulink Design Verifier Reports Approximations Through Validation Results.
The analysis is unable to confirm the satisfied status through validation results. For more information, see Objectives Satisfied - Needs Simulation.

Property proving

For the highlighted model object,

The analysis did not decide at least one proof objective. This situation can occur when:
- The analysis is still in progress.
- The analysis times out.
- A proof objective exists on a signal whose value the software cannot control, for example, a Constant block.
- The analysis cannot decide a proof objective because of division by zero or nonlinear arithmetic.
- The software cannot decide a proof objective because of stubbing. For more information, see Handle Incompatibilities with Automatic Stubbing.
- The software cannot decide a proof objective because of limitations of the analysis engine. For example, if the analysis encounters an unbounded while loop, it performs an approximation. For more information, see Role of Approximations During Model Analysis.

The analysis found valid objectives that approximations can impact. For more information, see How Simulink Design Verifier Reports Approximations Through Validation Results.
The software is unable to confirm the falsified status through validation results. For more information, see Objectives Falsified - Needs Simulation.

Gray Highlighting on Model

Objects that are highlighted in gray have the following meaning.

Analysis Mode	Gray Highlighting
Design error detection Test generation Property proving	The model object was not part of the analysis.