Role of Approximations During Model Analysis
The Simulink^{®} Design Verifier™ software generates inputs and parameters to achieve objectives. However, there can 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 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, suppose the software generates a test case signal that should achieve an objective by exceeding a threshold, a floatingpoint roundoff 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:
FloatingPoint to Rational Number Conversion
In some cases, the Simulink Design Verifier software simplifies the linear arithmetic of floatingpoint numbers by approximating them with infiniteprecision 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 floatingpoint 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:
Roundoff error is not considered.
Upper and lower bounds of floatingpoint numbers are not considered.
If your model casts floatingpoint 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 floatingpoint 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 TwoDimensional Lookup Tables for FloatingPoint Data Types
The Simulink Design Verifier software does not support nonlinear arithmetic for floatingpoint data types. If your model contains any 2D Lookup Table blocks, or nD Lookup Table blocks where n = 2, with all of the following characteristics, the software approximates nonlinear twodimensional interpolation with linear interpolation by fitting planes to each interpolation interval.
Block  Characteristics 

nD Lookup Table block, n = 2: 

Approximation of One and TwoDimensional Lookup Tables for Integer and FixedPoint 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 evenlyspaced in each of their respective dimensions.
Block  Characteristics 

nD Lookup Table block, n = 1 or n = 2: 

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 Mode  While Loop Approximation 

Design Error Detection  Sets number of while loop iterations to 3.
Does not report dead logic or valid objectives. 
Test Case Generation  Sets number of while loop iterations to 3.
Does not report unsatisfiable objectives. 
Property Proving  Sets number of while loop iterations to 3.
Does not report valid objectives. 
See Also
How Simulink Design Verifier Reports Approximations Through Validation Results  Review Analysis Results