Main Content

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.

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.

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');

approximations_example.png

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

approximations_test_generation_results.png

Test Objectives Status - Objective Undecided with Testcases

approximations_test_generation_results1.png

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

approximations_prove_properties_results.png

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