Learn more about Simulink Design Verifier

Approximations

On this page…
Approximations During Model Analysis Types of Approximations Converting Floating-Point Arithmetic to Rational-Number Arithmetic Linearizing 2-D Lookup Tables Unrolling While Loops Ensuring the Validity of the Analysis

Approximations During Model Analysis

The Simulink Design Verifier software attempts to generate inputs and parameters to achieve test and proof 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.

Back to Top

Types of Approximations

Simulink Design Verifier software performs three types of approximations when it analyzes a model:

• Converting Floating-Point Arithmetic to Rational-Number Arithmetic

• Linearizing 2-D Lookup Tables

• Unrolling While Loops

Back to Top

Converting Floating-Point Arithmetic to Rational-Number Arithmetic

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 proof and test 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, the Simulink Design Verifier software converts those values to rational numbers before performing its analysis.

Note   As a result of these approximations, Simulink Design Verifier software does not consider the effect of round-off error, or the upper and lower bounds of floating-point numbers.

Back to Top

Linearizing 2-D Lookup Tables

The Simulink Design Verifier software does not support nonlinear arithmetic. If your model contains any Lookup Table (2-D) blocks, the software approximates nonlinear 2-D interpolation with linear interpolation by fitting planes to each interpolation interval, if necessary.

Back to Top

Unrolling While Loops

If your model or any Stateflow chart in your model contains a while loop, the Simulink Design Verifier software tries to find a bound that allows the while loop to exit. To find a bound, it unrolls the while loop and executes it three times. If the software does not find a bound for a test case generation analysis, it sets the number of loop iterations to three for the purpose of the analysis. If you are performing a property-proving analysis, the analysis terminates.

Back to Top

Ensuring the Validity of the Analysis

The Simulink Design Verifier software records all approximations it performed in the Analysis Information chapter of the HTML report. (For a description of the contents 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 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.

Back to Top

Handling Incompatibilities with Automatic Stubbing

Ensuring Compatibility with the Simulink Design Verifier Software

© 1984-2009- The MathWorks, Inc.    -   Site Help   -   Patents   -   Trademarks   -   Privacy Policy   -   Preventing Piracy   -   RSS