5 / 16
Разработка и исследование синтетического метода верификации программы…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
53
Рис. 1.
Задание функции и ее бинарное решающее дерево
Третий вариант диаграммы является конечным для функции
.
f
Такое
представление является более компактным, чем таблица истинности и ее би-
нарное дерево (рис. 2).
Рис. 2.
BDD после первого (слева), второго (в центре), третьего (справа) правил сжатия
При применении бинарных решающих диаграмм становится возможным
решать проблемы, которые при традиционном представлении структур нераз-
решимы.
Такие логические операции (конъюнкция, дизъюнкция, отрицание) могут
быть проведены непосредственно над BDD с помощью алгоритмов, выполняю-
щих манипуляции над графами за полиномиальное время. Однако повторение
этих операций множество раз, например, при формировании конъюнкций или
дизъюнкций набора, могут привести к экспоненциально большому BDD в худ-
шем случае. Это происходит из-за того, что результатом любых предшествую-
щих операций над двумя BDD в общем случае может быть BDD с размером,
пропорциональным произведению предшествующих размеров, поэтому для
нескольких BDD размер может увеличиваться экспоненциально.
Методы оптимизации процесса верификации моделей большого разме-
ра.
Для верификации моделей большего размера реализован ряд алгоритмов
оптимизации, которые соответственно их методике подразделяются на две раз-
личные группы:
оптимизации, позволяющие сократить число достижимых состояний мо-
дели за счет редукции частичных порядков и объединения операторов;
оптимизации, позволяющие уменьшить объем памяти, занимаемой век-
торами состояний.
Метод редукции частичных порядков.
Редукция частичных порядков
позволяет вместо всех полученных на основе интерливинга вариантов выпол-