Role of Approximations During Model Analysis

The Simulink^® Design Verifier™ software generates inputs and parameters to achieve objectives. However, there can be a large number of values for the software to search. To create reasonable limits on the analysis, the software performs approximations to simplify the analysis. The software records all the approximations it performed in the Analysis Information chapter of the Simulink Design Verifier HTML report. For a description of this chapter, see Analysis Information Chapter.

Review the analysis results carefully when the software uses approximations. Evaluate your model to identify which blocks or subsystems caused the software to perform the approximations.

In rare cases, an approximation can result in test cases that fail to achieve test objectives or demonstrate a design error, or counterexamples that fail to falsify proof objectives. For example, when the software generates a test case signal that should achieve an objective by exceeding a threshold, a floating-point round-off error might prevent that signal from attaining the threshold value. For more information, see How Simulink Design Verifier Reports Approximations Through Validation Results.

Types of Approximations

The Simulink Design Verifier software performs the following approximations when it analyzes a model:

Floating-Point to Rational Number Conversion

In some cases, the Simulink Design Verifier software simplifies the linear arithmetic of floating-point numbers by approximating them with infinite-precision rational numbers. The software discovers how the logical relationships between these values affect the objectives. This analysis enables the software to support supervisory logic that is commonly found in embedded controller designs. For an example, see Identify the Effect of Approximations Through Validation Results.

If your model contains floating-point values in the signals, input values, or block parameters, Simulink Design Verifier converts some values to rational numbers before performing its analysis. As a result of these approximations:

Round-off error is not considered.
Upper and lower bounds of floating-point numbers are not considered.
If your model casts floating-point values to integer values, the integer representation can affect tests generated for the model. In some rare cases, the generated tests might not satisfy objectives associated with the floating-point values.

Note

You can use the Run additional analysis to reduce instances of rational approximation option in the Configuration parameters window to reduce instances of approximation. For more information, see Run Additional Analysis to Reduce Instances of Rational Approximation.

Linearization of Two-Dimensional Lookup Tables for Floating-Point Data Types

The software approximates nonlinear two-dimensional interpolation with linear interpolation by fitting planes to each interpolation interval when your model contains 2-D Lookup Table blocks, or n-D Lookup Table blocks where n = 2, with these characteristics:

Interpolation method parameter is Linear.
Extrapolation method parameter is Clip or Linear.
The input and output signals both have the floating-point data type.

Approximation of One- and Two-Dimensional Lookup Tables for Integer and Fixed-Point Data Types

If your model contains lookup tables with the following characteristics, Simulink Design Verifier automatically converts your original lookup table into a new lookup table composed of breakpoints that are evenly-spaced in each of their respective dimensions, with these characteristics:

Interpolation method parameter is Linear.
Extrapolation method parameter is Clip.
Index search method parameter is Linear search or Binary search.
The input and output signals are both of the same type and are both integer type or fixed-point type.

This approximation allows Simulink Design Verifier to generate tests significantly faster. The time saved is pronounced when you have unsatisfiable test objectives in your model.

`while`-Loop Approximations

If your model contains a while-loop, for each while-loop in the model, Simulink Design Verifier tries to detect a conservative constant upper bound on the number of iterations of the while-loop that is necessary to perform the analysis. If the software cannot find a constant bound, it sometimes performs a while-loop approximation. When the software uses a while-loop approximation this approximation is used to prove objectives valid or unsatisfiable, it reports the objectives as valid under approximation or unsatisfiable under approximation.

Model Blocks

If your model contains Model blocks that reference external models, test creation occurs for the top-level model, considering each referenced model in its execution context.

If multiple Model blocks reference the same model, generated tests attempt to satisfy test objectives for each instance of the referenced model in its individual context in the top-level model. If you have three Model blocks that reference a certain model, the analysis produces results for all three instances.

If you collect coverage using the generated test cases, the cumulative coverage reflects the multiple instances of the same referenced model. The simulation produces one set of coverage results for each referenced model; if you have three Model blocks that reference a certain model, the simulation produces one set of results for that referenced model.

For example, consider a top-level model with three Model blocks referencing the same model. The referenced model has three test objectives. Analyzing the top-level model produces nine test objectives. If you simulate the model with the nine test cases, the coverage results for that referenced model specify three test objectives.