Understanding Objective Statuses
R2026bFor every analysis mode, Simulink® Design Verifier™ assigns and evaluates objective statuses, such as satisfied, falsified, or undecided, to show you clearly whether specific design requirements or test conditions have been met, violated, or remain unresolved. This allows you to identify which areas of your model need more attention, helping you ensure thorough verification throughout the development process.
Test Generation Objective Statuses
This table explains how objective statuses are determined in test‑generation mode along with their corresponding supporting data, such as the associated test inputs:
Objective Status | Supporting Data | Description |
Satisfied | Test inputs |
|
Satisfied by Coverage Data | Not applicable | This objective is marked as covered in the input coverage data for the analysis. |
Satisfied by Existing Test case | Test inputs | The test inputs you provide satisfy the objective. |
Satisfied - Needs Simulation | Test inputs |
|
Satisfied - No Test case | Not applicable | This objective is satisfied when simulating the model. |
Undecided due to Runtime Error |
| Simulating the test inputs triggers a run-time error that prevents the generation of coverage data. The error details identify the model element responsible for the issue during simulation. For more information, see Resolve Undecided Objective Statuses Caused by Possible Modeling Errors and Address Undecided due to Runtime Error in Simulink Design Verifier Analysis. |
Undecided with Test case | Test inputs | The test inputs miss to cover this objective during simulation. In most cases this happens due to effects of approximations introduced during analysis. For more information, see Understanding Result Approximations. |
Unsatisfiable | Not applicable |
|
Unsatisfiable under Approximation | Not applicable |
|
Justified, Excluded | Not applicable | Objective removed by filter or justification. |
Design Error Detection Objective Statuses
This table provides explanation on the statuses for dead logic analysis for model coverage objectives along with their corresponding supporting data, such as the associated test inputs:
Coverage Objective Status | Supporting Data | Description |
Dead Logic | Not applicable |
|
Active Logic | Test inputs |
|
Active Logic - Needs Simulation | Test inputs |
|
Dead Logic under approximation | Not applicable |
|
Justified, Excluded | Not applicable | Objective removed by filter or justification. |
This table provides an explanation of statuses related to modeling errors, such as out-of-bound array access, numerical errors, such as division by zero, signal range errors such as, violations of specified minimum or maximum values, and high-integrity systems modeling checks such as, the use of remainder and reciprocal operations, HISL-002.
Modeling Error Objective Status | Supporting Data | Description |
Valid | Not applicable | No test input data can ever reach the modelling error defined by the objective. |
Falsified | Test inputs | The given test inputs exercise the run-time error during simulation. |
Falsified - needs simulation | Test inputs | To reproduce the design error corresponding to the given objective, you can generate harness for simulation purpose. |
Falsified - No Counterexample | Not applicable | The error is exercised when the model is simulated. |
Valid under approximation | Not applicable | The design error corresponding to given objective can probably never occur. The result is impacted by approximations. For more information on approximations, see Approximations During Model Analysis. |
Undecided Possibly Due to Long Counterexample | Minimum length of counterexample | The modeling error may only appear when you simulate with very long
test inputs. The counterexample requires the number of steps mentioned in the
column |
Property Proving Objective Statuses
This table provides explanation on the statuses for property proving objectives along with their corresponding supporting data, such as the associated test inputs:
Proof Objective Status | Supporting Data | Description |
Valid | Not applicable | The property specified by the Proof Objective is always satisfied. |
Falsified | Test inputs | The given test inputs exercise the run-time error during simulation. |
Falsified - needs simulation | Test inputs | To determine if the proof objective is falsified, you must simulate test inputs by enabling model coverage for custom objectives and inspect coverage data. |
Falsified - No Counterexample | Not applicable | The error is exercised when the model is simulated. |
Valid under approximation | Not applicable | The condition specified by the proof objective will almost always hold true. However, the result may be affected by approximations. |
Undecided with Counterexamples | Test inputs | The test inputs fail to falsify the Proof Objective is falsified when the model is simulated using provided test inputs or counterexample. In most cases, the coverage data generated by simulating the provided test input indicates that the condition defined by the proof objective has been met. In most cases, this occurs due to the effects of approximations made during the analysis. For more information, see Understanding Result Approximations |
Common Objectives Status
If Simulink Design Verifier analysis cannot conclusively determine outcomes for the objectives, it produces incomplete results. In the results summary, these incomplete results show that the objectives are undecided objectives, which often arise from model complexity, unsupported features, or analysis limitations. For more information on how to analyze and resolve these objective status, see Analyze and Resolve Undecided Objective Statuses.
This table provides explanation on the common objective statuses along with their corresponding supporting data, such as the associated test inputs:
Objective Status | Supporting Data | Description |
Undecided Due to Stubbing | List of model elements that are stubbed. | Upstream stubbing makes the status inconclusive. Simulink Design Verifier may introduce this stubbing either while computing the model representation or during a substep of the analysis. For more information, see Handle Model Complexities with Automatic Stubbing. |
Undecided Due to Nonlinearities | Not applicable | Nonlinear arithmetic in the upstream part of the design makes the status inconclusive. |
Undecided Due to Division by Zero | Not applicable | Some upstream computations in the design may keep downstream objectives from reaching a decision. |
Undecided Due to Array Out of Bounds | Test inputs | Some upstream computations in the design may keep downstream objectives from reaching a decision. |
Undecided | Not applicable | The result is inconclusive. |
See Also
Review Results from Analysis Report