## Reporting 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 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 ModeObjectives Status

Design error detection

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:

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 ModeObjectives Status

Design error detection

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.

2. To perform test generation analysis, on the Design Verifier tab, click . 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 . Click .

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

Th `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`.