Main Content

Approximations

Approximations During Model Analysis

The Simulink® Design Verifier™ software attempts to generate inputs and parameters to achieve objectives. However, there could be an infinite 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 any 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.

Rarely, 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, suppose 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.

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 affects the objectives. This analysis enables the software to support supervisory logic that is commonly found in embedded controls designs.

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 may not satisfy objectives associated with the floating-point values.

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

The Simulink Design Verifier software does not support nonlinear arithmetic for floating-point data types. If your model contains any 2-D Lookup Table blocks, or n-D Lookup Table blocks where n = 2, with all of the following characteristics, the software approximates nonlinear two-dimensional interpolation with linear interpolation by fitting planes to each interpolation interval.

BlockCharacteristics

n-D Lookup Table block, n = 2:

  • 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 of 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.

BlockCharacteristics

n-D Lookup Table block, n = 1 or n = 2:

  • 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.

If Simulink Design Verifier applies such approximations to your model, the Simulink Design Verifier report includes details of the approximation.

While Loops

If your model or a Stateflow® chart in your model contains a while loop, Simulink Design Verifier tries to detect a conservative constant bound that allows the while loop to exit. If the software cannot find a constant bound, it performs a while loop approximation. With this approximation, the analysis does not prove objectives to be valid or unsatisfiable and it does not prove dead logic. The generated analysis report notes this approximation.

The behavior of the while loop approximation is consistent in all modes of analysis, as described in the following table.

Analysis ModeWhile Loop Approximation
Design Error DetectionSets number of while loop iterations to 3. Does not report dead logic or valid objectives.
Test Case GenerationSets number of while loop iterations to 3. Does not report unsatisfiable objectives.
Property ProvingSets number of while loop iterations to 3. Does not report valid objectives.