1294
правки
Бинарный граф решений: различия между версиями
Перейти к навигации
Перейти к поиску
→Литература
Irina (обсуждение | вклад) |
KVN (обсуждение | вклад) |
||
| (не показаны 3 промежуточные версии 2 участников) | |||
| Строка 1: | Строка 1: | ||
Ключевые слова и синонимы: | Ключевые слова и синонимы: '''БДР'''; '''бинарная диаграмма решений''' | ||
== Постановка задачи == | == Постановка задачи == | ||
'''Булевы функции''' | '''Булевы функции''' | ||
Понятие | Понятие ''булевой функции'' – функции с областью определения {0,1}<math>^n</math> и областью значений {0,1} – является одним из базовых понятий для любых вычислений. Булевы функции используются в основополагающих работах по вычислительной сложности [7, 9], а также при проектировании и анализе логических схем [4, 13]. Булева функция может быть представлена в виде ''таблицы истинности'' – перечисления значений, принимаемых функцией на каждом элементе {0,1}<math>^n</math>. Поскольку для представления в виде таблицы истинности требуется экспоненциальный относительно n объем памяти, для большинства приложений оно оказывается непрактичным. Следовательно, существует потребность в структурах данных и соответствующих алгоритмах для эффективного представления и обработки булевых функций. | ||
'''Булевы схемы''' | '''Булевы схемы''' | ||
Булевы функции могут быть представлены различными способами. Одним из естественных представлений является | Булевы функции могут быть представлены различными способами. Одним из естественных представлений является ''схема булевых комбинаций'', или просто ''булева схема'' [6, глава 34]. Схема состоит из булевых комбинационных элементов, соединенных ''проводами''. Булевыми комбинационными элементами являются ''вентили'' и ''первичные входы''. Существуют три типа вентилей: NOT, AND и OR. Вентильная функция NOT работает следующим образом: она принимает одно булево ''значение-вход'' и вычисляет одно булево ''значение-выход'', которое принимает значение 0 в случае, если вход равен 1, и 1 – если вход равен 0. Вентиль AND принимает два булевых значения-входа и вычисляет одно значение-выход, равное 1, если оба входа имеют значение 1, и 0 в противном случае. Вентиль OR похож на AND, за тем исключением, что выходное значение равно 1 в случае, если одно или оба входных значения равны 1, и 0 в противном случае. | ||
Схемы должны быть бесконтурными; отсутствие контуров обеспечивает возможность однозначным образом протягивать булево присваивание первичным входам по вентилям в топологическом порядке. Из этого следует, что схема на n упорядоченных первичных входах с выделенным вентилем, называемым | Схемы должны быть бесконтурными; отсутствие контуров обеспечивает возможность однозначным образом протягивать булево присваивание первичным входам по вентилям в топологическом порядке. Из этого следует, что схема на n упорядоченных первичных входах с выделенным вентилем, называемым ''первичным выходом'', соответствует булевой функции на {0,1}<math>^n</math>. Каждая булева функция может быть представлена схемой – например, путем построения схемы, воспроизводящей таблицу истинности. | ||
Представление в виде схемы имеет слишком общий вид: любая проблема разрешимости, вычислимая на машине Тьюринга за полиномиальное время, может быть вычислена при помощи схем полиномиальной относительно размера экземпляра величины, причем схемы могут быть эффективно построены из программы машины Тьюринга [15]. Однако главные задачи анализа на схемах, называемые проблемой выполнимости и проблемой эквивалентности, являются NP-полными [7]. | Представление в виде схемы имеет слишком общий вид: любая проблема разрешимости, вычислимая на [[Машина Тьюринга|машине Тьюринга]] за полиномиальное время, может быть вычислена при помощи схем полиномиальной относительно размера экземпляра величины, причем схемы могут быть эффективно построены из программы машины Тьюринга [15]. Однако главные задачи анализа на схемах, называемые проблемой выполнимости и проблемой эквивалентности, являются [[NP-Полная задача|NP-полными]] [7]. | ||
'''Булевы формулы''' | '''Булевы формулы''' | ||
''Булева формула'' определяется рекурсивным образом: ''булева переменная'' <math>x_i</math> является булевой формулой; если <math>\varphi \,</math> и <math>\psi \, </math> являются булевыми формулами, то ими являются также (<math>\lnot \varphi</math>), (<math>\varphi \land \psi </math>), (<math>\varphi \lor \psi </math>), (<math>\varphi \rightarrow \psi </math>) и (<math>\varphi \leftrightarrow \psi </math>). Операторы <math>\lnot</math>, <math>\land</math>, <math>\lor</math>, <math>\rightarrow</math>, <math>\leftrightarrow</math> называются ''логическими операциями''; ради удобства записи скобки часто опускаются. Булевы формулы могут использоваться для представления произвольных булевых функций; однако проблемы выполнимости и эквивалентности формул также являются NP-полными. Булевы формулы являются менее краткими и сжатыми, чем булевы схемы: к примеру, функция четности имеет схемы линейного размера, тогда как представления в виде формул являются сверхполиномиальными. Точнее говоря, XOR<math>_n</math>: {0, 1}<math>^n</math> <math>\mapsto</math> {0, 1} определена следующим образом: она принимает значение 1 в точности на тех элементах {0, 1}<math>^n</math>, которые содержат нечетное число единиц. Определим ''размер'' формулы, равный количеству встречающихся в ней логических операций. Тогда для любой последовательности формул <math>\theta _1 \, </math>, <math>\theta _2 \, </math>, ... , такой, что <math>\theta _k \, </math> представляет XOR<math>_k</math>, размер <math>\theta _k \, </math> равен <math>\Omega(k^c) \, </math> для всех <math>c \in Z^+ \, </math> [14 , главы 11 и 12]. | |||
''Дизъюнкция'' представляет собой булеву формулу, содержащую только логические операции <math>\land</math> и <math>\lnot</math>, причем применяется только к переменным; к примеру, x1 <math>\land</math> <math>\lnot</math>x3 <math>\land</math> <math>\lnot</math>x5 является дизъюнкцией. Булева формула находится в ''дизъюнктивной нормальной форме'' (''ДНФ''), если она имеет вид <math>D_0 \lor D_1 \lor ... \lor D_{k-1}</math>, где каждый член <math>D_i</math> является дизъюнкцией. ДНФ-формулы могут представлять произвольные булевы функции, например, путем определения каждого входа, на котором формула принимает значение 1, как дизъюнкции. ДНФ-формулы применяются в проектировании логических схем, поскольку могут быть непосредственно переведены в ПЛМ [4]. Однако если проблема выполнимости ДНФ-формул решается тривиально, то проблема эквивалентности является [[NP-Полная задача|NP-полной]]. Кроме того, если <math>\varphi \, </math> и <math>\psi \,</math> являются ДНФ-формулами, то <math>\lnot \varphi </math> и <math>\varphi \land \psi </math> таковыми не являются, а перевод их в ДНФ, представляющие ту же функцию, может привести к экспоненциальному росту размера формулы. | |||
'''Деревья Шеннона''' | '''Деревья Шеннона''' | ||
Пусть f – булева функция на области определения {0,1}<math>^n</math>. Ассоциируем n размерностей с переменными <math>x_0, ..., x_{n-1}</math>. Тогда | Пусть f – булева функция на области определения {0,1}<math>^n</math>. Ассоциируем n размерностей с переменными <math>x_0, ..., x_{n-1}</math>. Тогда ''положительным сомножителем'' f относительно <math>x_i</math>, обозначаемым <math>f_{xi}</math>, является функция на области определения {0,1}<math>^n</math>, которая задается следующим образом | ||
<math>f_{xi}( \alpha_0, ... , \alpha_{i-1}, \alpha_i, \alpha_{i+1}, ..., \alpha_{n-1}) = f( \alpha_0, ... ,\alpha_{i-1}, 1, \alpha_{i+1}, ..., \alpha_{n-1}) \, </math>. | <math>f_{xi}( \alpha_0, ... , \alpha_{i-1}, \alpha_i, \alpha_{i+1}, ..., \alpha_{n-1}) = f( \alpha_0, ... ,\alpha_{i-1}, 1, \alpha_{i+1}, ..., \alpha_{n-1}) \, </math>. | ||
''Отрицательный сомножитель'' относительно <math>x_i</math>, обозначаемый <math>f_xi’</math>, определяется точно так же, только на правой стороне вместо 1 стоит 0. | |||
Каждая булева функция может быть подвергнута декомпозиции при помощи теоремы расширения Шеннона: | Каждая булева функция может быть подвергнута декомпозиции при помощи теоремы расширения Шеннона: | ||
| Строка 36: | Строка 36: | ||
Дерево Шеннона нельзя назвать достаточно удобным представлением, поскольку высота дерева, представляющего любую булеву функцию на {0,1}<math>^n</math>, равна n, так что дерево имеет <math>2^n</math> листьев. Дерево Шеннона можно уменьшить при помощи слияния изоморфных поддеревьев и пренебрежения вершинами, имеющими идентичных потомков. На первый взгляд, использование сокращенного дерева Шеннона тоже не особенно практично, поскольку оно включает создание на первом этапе полного бинарного дерева. Более того, пока неясно, как можно на сокращенном дереве Шеннона эффективно производить такие операции, как проверка эквивалентности или вычисление конъюнкции функций, представленных в виде сокращенных деревьев Шеннона. | Дерево Шеннона нельзя назвать достаточно удобным представлением, поскольку высота дерева, представляющего любую булеву функцию на {0,1}<math>^n</math>, равна n, так что дерево имеет <math>2^n</math> листьев. Дерево Шеннона можно уменьшить при помощи слияния изоморфных поддеревьев и пренебрежения вершинами, имеющими идентичных потомков. На первый взгляд, использование сокращенного дерева Шеннона тоже не особенно практично, поскольку оно включает создание на первом этапе полного бинарного дерева. Более того, пока неясно, как можно на сокращенном дереве Шеннона эффективно производить такие операции, как проверка эквивалентности или вычисление конъюнкции функций, представленных в виде сокращенных деревьев Шеннона. | ||
Брайант [5] пришел к выводу, что накладывание ограничения, согласно которому переменные появляются в фиксированном порядке от корня к листьям, значительно снижает сложность обработки сокращенных деревьев Шеннона. Это представление он назвал бинарной диаграммой решений (БДР). | Брайант [5] пришел к выводу, что накладывание ограничения, согласно которому переменные появляются в фиксированном порядке от корня к листьям, значительно снижает сложность обработки сокращенных деревьев Шеннона. Это представление он назвал ''бинарной диаграммой решений'' (БДР). | ||
== Основные результаты == | == Основные результаты == | ||
'''Определения''' | '''Определения''' | ||
Бинарная диаграмма решений (БДР) представляет собой бесконтурный орграф с выдеренной вершиной и не более чем двумя стоками, один из которых имеет метку 0, а другой – метку 1. Вершины, не являющиеся стоками, помечены переменными. Каждая вершина, не являющаяся стоком, имеет две исходящих дуги; одна из них имеет метку 1 и ведет к ''1-потомку'', другая имеет метку 0 и ведет к ''0-потомку''. Переменные должны быть упорядочены; иначе говоря, если переменная-метка <math>x_i</math> появляется раньше метки <math>x_j</math> на некотором пути из вершины к стоку, тогда метка <math>x_j</math> не может встречаться до <math>x_i</math> ни на одном пути из вершины к стоку. Две вершины являются | Бинарная диаграмма решений (БДР) представляет собой бесконтурный орграф с выдеренной вершиной и не более чем двумя стоками, один из которых имеет метку 0, а другой – метку 1. Вершины, не являющиеся стоками, помечены переменными. Каждая вершина, не являющаяся стоком, имеет две исходящих дуги; одна из них имеет метку 1 и ведет к ''1-потомку'', другая имеет метку 0 и ведет к ''0-потомку''. Переменные должны быть упорядочены; иначе говоря, если переменная-метка <math>x_i</math> появляется раньше метки <math>x_j</math> на некотором пути из вершины к стоку, тогда метка <math>x_j</math> не может встречаться до <math>x_i</math> ни на одном пути из вершины к стоку. Две вершины являются ''изоморфными'', если обе являются стоками с одинаковой меткой либо представляют собой вершины, не являющиеся стоками, с одной и той же переменной-меткой, причем их 0-потомки и 1-потомки изоморфны. Чтобы бесконтурный орграф был допустимой БДР, необходимо, чтобы в нем не было изоморфных вершин и чтобы никакие вершины не имели одинаковых 0-потомков и 1-потомков. | ||
Основной результат теории БДР заключается в следующем: если дано фиксированное упорядочение переменных, то представление является уникальным с точностью до изоморфизма. Иначе говоря, если F и G являются БДР, представляющими f: {0, 1}<math>^n</math> <math>\mapsto</math> {0, 1} с порядком переменных <math>x_1 \prec x_2 \prec ... x_n</math>, то F и G являются изоформными. | Основной результат теории БДР заключается в следующем: если дано фиксированное упорядочение переменных, то представление является уникальным с точностью до изоморфизма. Иначе говоря, если F и G являются БДР, представляющими f: {0, 1}<math>^n</math> <math>\mapsto</math> {0, 1} с порядком переменных <math>x_1 \prec x_2 \prec ... x_n</math>, то F и G являются изоформными. | ||
| Строка 66: | Строка 66: | ||
Вентили, составляющие конструкцию, часто обновляются в силу эксплуатационных требований; эти изменения обычно не предполагают изменения логической функциональности конструкции. Подходы, основанные на использовании БДР, применяются для проверки эквивалентности при проектировании цифрового оборудования [10]. | Вентили, составляющие конструкцию, часто обновляются в силу эксплуатационных требований; эти изменения обычно не предполагают изменения логической функциональности конструкции. Подходы, основанные на использовании БДР, применяются для проверки эквивалентности при проектировании цифрового оборудования [10]. | ||
БДР также используются для проверки свойств цифрового оборудования. Типичная формулировка выглядит следующим образом: имеются множество «хороших» состояний и множество «начальных» состояний, определенные при помощи булевых формул над элементами хранения состояния; свойство выполняется в том и только том случае, если не имеется последовательностей входных значений, которые приводят состояние в начальном состоянии в состояние, не входящее в множество хороших состояний. Если имеется конструкция с n регистрами, множество состояний A в конструкции может быть охарактеризовано формулой <math>\varphi_A</math> над n булевыми переменными: <math>\varphi_A</math> расценивает присваивание переменным как истинное в том и только том случае, если соответствующее состояние входит в множество A. Формула <math>\varphi_A</math> представляет булеву функцию; таким образом, для представления множеств состояний могут использоваться БДР. Основная операция вычисления образа множества состояний системы (то есть множества состояний, которые могут быть достигнуты при применении одного входного значения из состояний множества A) также может быть реализована с использованием БДР [12]. | БДР также используются для проверки свойств цифрового оборудования. Типичная формулировка выглядит следующим образом: имеются множество «хороших» состояний и множество «начальных» состояний, определенные при помощи булевых формул над элементами хранения состояния; свойство выполняется в том и только том случае, если не имеется последовательностей входных значений, которые приводят состояние в начальном состоянии в состояние, не входящее в множество хороших состояний. Если имеется конструкция с n регистрами, множество состояний A в конструкции может быть охарактеризовано формулой <math>\varphi_A</math> над n булевыми переменными: <math>\varphi_A</math> расценивает присваивание переменным как истинное в том и только том случае, если соответствующее состояние входит в множество A. Формула <math>\varphi_A</math> представляет булеву функцию; таким образом, для представления множеств состояний могут использоваться БДР. Основная операция вычисления ''образа'' множества состояний системы (то есть множества состояний, которые могут быть достигнуты при применении одного входного значения из состояний множества A) также может быть реализована с использованием БДР [12]. | ||
Бинарные диаграммы решений использовались также для генерации тестов. Один из подходов к генерации тестов заключается в задании допустимых входных значений при помощи ограничений, которые, в сущности, являются булевыми формулами над первичным входом и переменными состояния. Юань и коллеги [18] продемонстрировали высокую эффективность БДР в работе с подобными ограничениями. | Бинарные диаграммы решений использовались также для ''генерации тестов''. Один из подходов к генерации тестов заключается в задании допустимых входных значений при помощи ограничений, которые, в сущности, являются булевыми формулами над первичным входом и переменными состояния. Юань и коллеги [18] продемонстрировали высокую эффективность БДР в работе с подобными ограничениями. | ||
Синтез логических схем заключается в воплощении аппаратных конструкций, заданных логическими уравнениями, при помощи вентилей. Отображение уравнений на вентили производится тривиальным образом; однако на практике прямое отображение приводит к появлению конструкций, неприемлемых с точки зрения производительности (измеряемой площадью вентильной схемы или временной задержкой). Преобразование логических уравнений для сокращения площади (например, посредством протягивания констант, определения общих подвыражений и т.п.) или задержки (в частности, путем протягивания поздно приходящих сигналов ближе к точкам выхода) обычно производится при помощи БДР. | Синтез логических схем заключается в воплощении аппаратных конструкций, заданных логическими уравнениями, при помощи вентилей. Отображение уравнений на вентили производится тривиальным образом; однако на практике прямое отображение приводит к появлению конструкций, неприемлемых с точки зрения производительности (измеряемой площадью вентильной схемы или временной задержкой). Преобразование логических уравнений для сокращения площади (например, посредством протягивания констант, определения общих подвыражений и т.п.) или задержки (в частности, путем протягивания поздно приходящих сигналов ближе к точкам выхода) обычно производится при помощи БДР. | ||
| Строка 74: | Строка 74: | ||
== Экспериментальные результаты == | == Экспериментальные результаты == | ||
Брайант исследовал возможность проверки двух качественно различных схем для сложения. Ему удалось проверить эквивалентность двух 64-битных сумматоров на VAX 11/780 (компьютере с одним MIP) за 95,8 минут. При этом он использовал выведенное вручную упорядочение. | Брайант исследовал возможность проверки двух качественно различных схем для сложения. Ему удалось проверить эквивалентность двух 64-битных сумматоров на VAX 11/780 (компьютере с одним MIP) за 95,8 минут. При этом он использовал выведенное вручную упорядочение. | ||
Современные БДР-пакеты работают на два порядка величины быстрее, чем первая реализация Брайанта. Одним из источников усовершенствования было использование строгой канонической формы, в которой поддерживается глобальная база данных вершин БДР, и ни одна новая вершина не может быть добавлена без проверки, не существует ли уже в базе данных вершины с той же меткой и теми же 0-потомком и 1-потомком [3]. (Для этого требуется, чтобы потомки любой добавляемой вершины также находились в строгой канонической форме). Другими путями к повышению производительности были использование дополнительных указателей (если у указателя установлен наименьший значащий бит, он ссылается на дополнение функции), лучшее управление памятью (сборка мусора на базе счетчиков ссылок, хранение часто используемых вершин в памяти поблизости друг от друга), улучшенные хэш-функции и лучшая организация таблицы вычисленных результатов (в которой отслеживаются подзадачи, уже встреченные ранее) [16]. | |||
Современные БДР-пакеты работают на два порядка величины быстрее, чем первая реализация Брайанта. Одним из источников усовершенствования было использование ''строгой канонической формы'', в которой поддерживается глобальная база данных вершин БДР, и ни одна новая вершина не может быть добавлена без проверки, не существует ли уже в базе данных вершины с той же меткой и теми же 0-потомком и 1-потомком [3]. (Для этого требуется, чтобы потомки любой добавляемой вершины также находились в строгой канонической форме). Другими путями к повышению производительности были использование дополнительных указателей (если у указателя установлен наименьший значащий бит, он ссылается на дополнение функции), лучшее управление памятью (сборка мусора на базе счетчиков ссылок, хранение часто используемых вершин в памяти поблизости друг от друга), улучшенные хэш-функции и лучшая организация таблицы вычисленных результатов (в которой отслеживаются подзадачи, уже встреченные ранее) [16]. | |||
'''Наборы данных''' | '''Наборы данных''' | ||
Для синтеза логических схем используется система | Для синтеза логических схем используется система [http://embedded.eecs.berkeley.edu/pubs/downloads/sis/ SIS] из Калифорнийского университета в Беркли. Она содержит несколько комбинационных и последовательных схем, использовавшихся для эталонного тестирования пакетов БДР. | ||
Система | Система [http://embedded.eecs.berkeley.edu/pubs/downloads/vis VIS] из Калифорнийского университета в Беркли и Колорадского университета в Боулдере применяется для верификации проектов; она использует БДР для проведения проверок. Дистрибутив содержит большой пакет задач верификации, начиная с простых аппаратных схем до сложных мультипроцессорных систем с кэш-памятью. | ||
== Ссылка на код == | == Ссылка на код == | ||
В настоящее время доступно множество пакетов БДР; автор обзора рекомендует пакет | В настоящее время доступно множество пакетов БДР; автор обзора рекомендует пакет [http://vlsi.colorado.edu/~fabio/CUDD/ CUDD]. CUDD реализует все основные функции для работы с БДР и их вариации; он написан на C++ и снабжен полной документацией для пользователя и разработчика. | ||
== См. также == | == См. также == | ||
| Строка 89: | Строка 91: | ||
== Литература == | == Литература == | ||
1. Aziz, A., Tasiran,S.,Brayton,R.: BDD Variable Ordering for Interacting Finite State Machines. In: ACM Design Automation Conference, pp. 283-288. (1994) | 1. Aziz, A., Tasiran,S.,Brayton,R.: BDD Variable Ordering for Interacting Finite State Machines. In: ACM Design Automation Conference, pp. 283-288. (1994) | ||
2. Berman, C.L.: Ordered Binary Decision Diagrams and Circuit Structure. In: IEEE International Conference on Computer Design. (1989) | |||
3. Brace, K., Rudell, R., Bryant, R.: Efficient Implementation of a BDD Package. In: ACM Design Automation Conference. (1990) | |||
4. Brayton, R., Hachtel, G., McMullen, C., Sangiovanni-Vincentelli, A.: Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers (1984) | |||
5. Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transac. Comp. C-35,677-691 (1986) | |||
6. Cormen,T.H., Leiserson, C.E., Rivest, R.H., Stein, C.: Introduction to Algorithms. MIT Press (2001) | |||
7. Garey, M.R., Johnson, D.S.: Computers and Intractability. W.H. Freeman and Co. (1979) | |||
8. Gupta, A.: Formal Hardware Verification Methods: A Survey. Formal Method Syst. Des. 1,151-238 (1993) | |||
9. Karchmer, M.: Communication Complexity: A New Approach to Circuit Depth. MIT Press (1989) | |||
10. Kuehlmann, A., Krohm, F.: Equivalence Checking Using Cuts and Heaps. In: ACM Design Automation Conference (1997) | |||
11. Malik, S., Wang, A.R., Brayton, R.K., Sangiovanni-Vincentelli, A.: Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment. In: IEEE International Conference on Computer-Aided Design, pp. 6-9. (1988) | |||
12. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers (1993) | |||
13. De Micheli, G.: Synthesis and Optimization of Digital Circuits. McGraw Hill (1994) | |||
14. Schoning, U., Pruim, R.: Gems of Theoretical Computer Science. Springer (1998) | |||
15. Sipser, M.: Introduction to the Theory of Computation, 2nd edn. Course Technology (2005) | |||
16. [http://vlsi.colorado.edu/~fabio/ Somenzi, F.: Colorado University Decision Diagram Package]. | |||
17. Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM (2000) | |||
18. Yuan, J., Pixley, C., Aziz, A.: Constraint-Based Verfication. Springer (2006) | |||
[[Категория: Совместное определение связанных терминов]] | |||