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