Бинарный граф решений: различия между версиями

Булевы функции

Понятие булевой функции – функции с областью определения {0,1}n и областью значений {0,1} – является одним из базовых понятий для любых вычислений. Булевы функции используются в основополагающих работах по вычислительной сложности [7, 9], а также при проектировании и анализе логических схем [4, 13]. Булева функция может быть представлена в виде таблицы истинности – перечисления значений, принимаемых функцией на каждом элементе {0,1}n. Поскольку для представления в виде таблицы истинности требуется экспоненциальный относительно n объем памяти, для большинства приложений оно оказывается непрактичным. Следовательно, существует потребность в структурах данных и соответствующих алгоритмах для эффективного представления и обработки булевых функций.

Брайант [5] пришел к выводу, что накладывание ограничения, согласно которому переменные появляются в фиксированном порядке от корня к листьям, значительно снижает сложность обработки сокращенных деревьев Шеннона. Это представление он назвал бинарной диаграммой решений (БДР).

Определения

Бинарная диаграмма решений (БДР) представляет собой бесконтурный орграф с выдеренной вершиной и не более чем двумя стоками, один из которых имеет метку 0, а другой – метку 1. Вершины, не являющиеся стоками, помечены переменными. Каждая вершина, не являющаяся стоком, имеет две исходящих дуги; одна из них имеет метку 1 и ведет к 1-потомку, другая имеет метку 0 и ведет к 0-потомку. Переменные должны быть упорядочены; иначе говоря, если переменная-метка xi появляется раньше метки xj на некотором пути из вершины к стоку, тогда метка xj не может встречаться до xi ни на одном пути из вершины к стоку. Две вершины являются изоморфными, если обе являются стоками с одинаковой меткой либо представляют собой вершины, не являющиеся стоками, с одной и той же переменной-меткой, причем их 0-потомки и 1-потомки изоморфны. Чтобы бесконтурный орграф был допустимой БДР, необходимо, чтобы в нем не было изоморфных вершин и чтобы никакие вершины не имели одинаковых 0-потомков и 1-потомков.

Все симметричные функции на {0,1}n имеют БДР полиномиального относительно n размера, независимо от порядка переменных. Однако другие полезные функции (например, компараторы, мультиплексоры, сумматоры и вычитатели) могут быть представлены более эффективно, если правильно выбран порядок переменных. Эвристики для выбора упорядочения представлены, например, в [1, 2, 11]. Существуют функции, не имеющие полиномиальных БДР при любом порядке переменных – например, функция, представляющая n-й бит выходного значения мультиплексора, принимающего на вход два n-битных целых числа без знака [5]. Вегенер [17] приводит и другие примеры, доказывающие важность правильного выбора порядка переменных.

БДР чаще всего применяются в контексте формальной верификации цифрового оборудования [8]. Цифровое оборудование является расширением понятия схемы, описанного выше, путем введения элементов хранения состояния, которые хранят булево значение между обновлениями и обновляются по сигналу синхронизатора.

Вентили, составляющие конструкцию, часто обновляются в силу эксплуатационных требований; эти изменения обычно не предполагают изменения логической функциональности конструкции. Подходы, основанные на использовании БДР, применяются для проверки эквивалентности при проектировании цифрового оборудования [10].

Синтез логических схем заключается в воплощении аппаратных конструкций, заданных логическими уравнениями, при помощи вентилей. Отображение уравнений на вентили производится тривиальным образом; однако на практике прямое отображение приводит к появлению конструкций, неприемлемых с точки зрения производительности (измеряемой площадью вентильной схемы или временной задержкой). Преобразование логических уравнений для сокращения площади (например, посредством протягивания констант, определения общих подвыражений и т.п.) или задержки (в частности, путем протягивания поздно приходящих сигналов ближе к точкам выхода) обычно производится при помощи БДР.

Брайант исследовал возможность проверки двух качественно различных схем для сложения. Ему удалось проверить эквивалентность двух 64-битных сумматоров на VAX 11/780 (компьютере с одним MIP) за 95,8 минут. При этом он использовал выведенное вручную упорядочение.

Современные БДР-пакеты работают на два порядка величины быстрее, чем первая реализация Брайанта. Одним из источников усовершенствования было использование строгой канонической формы, в которой поддерживается глобальная база данных вершин БДР, и ни одна новая вершина не может быть добавлена без проверки, не существует ли уже в базе данных вершины с той же меткой и теми же 0-потомком и 1-потомком [3]. (Для этого требуется, чтобы потомки любой добавляемой вершины также находились в строгой канонической форме). Другими путями к повышению производительности были использование дополнительных указателей (если у указателя установлен наименьший значащий бит, он ссылается на дополнение функции), лучшее управление памятью (сборка мусора на базе счетчиков ссылок, хранение часто используемых вершин в памяти поблизости друг от друга), улучшенные хэш-функции и лучшая организация таблицы вычисленных результатов (в которой отслеживаются подзадачи, уже встреченные ранее) [16].

Система VIS (http://embedded.eecs.berkeley.edu/pubs/ downloads/vis) из Калифорнийского университета в Беркли и Колорадского университета в Боулдере применяется для верификации проектов; она использует БДР для проведения проверок. Дистрибутив содержит большой пакет задач верификации, начиная с простых аппаратных схем до сложных мультипроцессорных систем с кэш-памятью.

В настоящее время доступно множество пакетов БДР; автор обзора рекомендует пакет CUDD (http://vlsi.colorado.edu/~fabio/ CUDD/). CUDD реализует все основные функции для работы с БДР и их вариации; он написан на C++ и снабжен полной документацией для пользователя и разработчика.

► Символьная проверка на модели

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. Somenzi, F.: Colorado University Decision Diagram Package. http://vlsi.colorado.edu/~fabio/

17. Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM (2000)

18. Yuan, J., Pixley, C., Aziz, A.: Constraint-Based  Verfication. Springer (2006)