How Simulink Design Verifier Reports Approximations Through Validation Results

Simulink^® Design Verifier™ performs approximations during analysis. The software identifies the presence of approximations and reports them at the level of each objective status in the Objective Status Chapter of the Simulink Design Verifier HTML report. For more information, see Role of Approximations During Model Analysis and Objectives Status Chapters.

To validate the test cases or counterexamples during simulation, the model is locked in fast restart mode. For more information, see Fast Restart Methodology.

For example, to ensure the effect of approximations, in the test generation analysis the test cases are validated against the coverage data during analysis.

Impact of Approximations on Objectives Status

The software provides the test cases or counterexamples for the objectives that are impacted due to approximations during analysis. These objectives are reported as Objectives Undecided with Testcases for test generation analysis and Objectives Undecided with Counterexamples for property-proving analysis.

The software confirms the objectives that can be impacted due to approximations as dead logic, valid, or unsatisfiable. This table summarizes these objectives for all analysis modes.

Analysis Mode	Objectives Status
Design error detection	Dead Logic under Approximation Objectives Valid under Approximation
Test generation	Objectives Unsatisfiable under Approximation
Property proving	Objectives Valid under Approximation

The software is unable to confirm the objectives status through validation results for these cases:

• The objectives introduced by the block replacement. For more information, see What Is Block Replacement?.

• The Verification Subsystem consists of the sldv.test or sldv.prove function.

• You abort the analysis by using the Stop button in the Simulink Design Verifier Results Summary window or the software exceeds its Maximum analysis time. Therefore, some objectives remain unvalidated during analysis and the software is unable to confirm the objectives status.

• The block with an objective is inside the Simulink test harness but outside the component under test. For more information, see Test Harness and Model Relationship (Simulink Test).

This table summarizes the objectives statuses for the preceding cases. To confirm the status of the objectives, you must run additional simulations of test cases or counterexamples.

Analysis Mode	Objectives Status
Design error detection	Active Logic - Needs Simulation Objectives Error - Needs Simulation
Test generation	Objectives Satisfied - Needs Simulation
Property proving	Objectives Falsified - Needs Simulation

Identify the Effect of Approximations Through Validation Results

This example shows how approximations affect the objectives status of the Switch block. In the sldvApproximationsExample model, the calculations 1./3 and 2./3 in the Constant block result in Floating-Point to Rational Number Conversion during analysis.

For inport In2 equal to -1, the input 2 of the Switch block is not equal to 0 during simulation. Therefore, the Switch does not select inport In3 as output. For test generation and property-proving analysis, the objective logical trigger input false(output is from 3rd input port) for the Switch block is undecided due to the impact of approximations during analysis.

1. Open the model sldvApproximationsExample:

open_system('sldvApproximationsExample');

2. To perform test generation analysis, on the Design Verifier tab, click Generate Tests. The software simulates the model and validates the test results against coverage data.

3. To view the detailed analysis report, click HTML in the Simulink® Design Verifier™ Results Summary window.

This image shows the Test Objectives Status section of the generated analysis report. The software provides two test cases that are impacted by approximations.

Test Objectives Status - Objective Satisfied

Test Objectives Status - Objective Undecided with Testcases

4. To perform property proving analysis, on the Design Verifier tab, in the Mode section, select Property Proving. Click Prove Properties.

This image shows the Proof Objectives Status section of the generated analysis report.

Proof Objectives Status - Objective Undecided with Counterexamples

The software provides one counterexample that is impacted by approximations.

Note: The sldvApproximationsExample example model is preconfigured with the Run additional analysis to reduce instances of rational approximation option set to Off. If you enable this option and run the analysis, the Undecided with Testcases test objective is reported as Unsatisfiable and the proof objective is reported as Valid.

Related Topics

• Review Results
• Role of Approximations During Model Analysis