Если у вас есть Simulink® моделируйте как с помощью логических, так и с помощью арифметических операций, рассмотрите анализ только логических операций.
Программное обеспечение Simulink Design Verifier™ не поддерживает нелинейную арифметику чисел с плавающей запятой, как это происходит с умножением или делением, если только один из операндов умножения или делитель не является константой.
Чтобы упростить модели, которые содержат целые числа или числа с плавающей запятой, программное обеспечение сопоставляет расчеты модели с выражениями логических переменных. Для примера программное обеспечение может представлять восьмибитное число как набор из восьми логических значений с одним для каждой цифры. Это может представлять бестолковое OR операция двух восьмибитных целых чисел как восьми отдельных логических OR операции.
Проблемы отображения одного типа данных в логические переменные сложны, и эта сложность увеличивается, когда программное обеспечение выполняет такое сопоставление. Программа обрабатывает модели с преимущественно логическими сигналами более эффективно, чем модели с сигналами с большим целым числом или с плавающей точкой.
Примечание
Программа Simulink Design Verifier может обрабатывать входы с плавающей точкой, когда их значения влияют на проект через линейные неравенства, такие как x < y или a > 0.
В сложение входа сложность может быть результатом определенных операций приведения. Для примера литье double в int8 может ввести нелинейность в определенных ситуациях.