If you have a Simulink® model with both logical and arithmetic operations, consider analyzing only the logical operations.
The Simulink Design Verifier™ software does not support nonlinear arithmetic of floating-point numbers, as occurs with multiplication or division, unless one of the multiply operands or the divisor is a constant.
To simplify models that contain integers or floating-point numbers,
the software maps the model computations into expressions of Boolean
variables. For example, the software might represent an eight-bit
number as a set of eight Boolean values, with one for each digit.
It might represent a bit-wise
OR operation of two
eight-bit integers as eight separate logical
Mapping problems of one data type into Boolean variables is complex, and this complexity increases when the software performs such mapping. The software handles models with predominantly logical signals more efficiently than it does those with large integer or floating-point signals.
Simulink Design Verifier software can handle floating-point inputs when their values impact the design through linear inequalities such as x < y or a > 0.
In addition, input complexity can result from certain cast operations. For
example, casting a
double to an
introduce a non-linearity in certain situations.