4551
правка
Бинарный граф решений: различия между версиями
Перейти к навигации
Перейти к поиску
→Применение
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 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] продемонстрировали высокую эффективность БДР в работе с подобными ограничениями. | ||
Синтез логических схем заключается в воплощении аппаратных конструкций, заданных логическими уравнениями, при помощи вентилей. Отображение уравнений на вентили производится тривиальным образом; однако на практике прямое отображение приводит к появлению конструкций, неприемлемых с точки зрения производительности (измеряемой площадью вентильной схемы или временной задержкой). Преобразование логических уравнений для сокращения площади (например, посредством протягивания констант, определения общих подвыражений и т.п.) или задержки (в частности, путем протягивания поздно приходящих сигналов ближе к точкам выхода) обычно производится при помощи БДР. | Синтез логических схем заключается в воплощении аппаратных конструкций, заданных логическими уравнениями, при помощи вентилей. Отображение уравнений на вентили производится тривиальным образом; однако на практике прямое отображение приводит к появлению конструкций, неприемлемых с точки зрения производительности (измеряемой площадью вентильной схемы или временной задержкой). Преобразование логических уравнений для сокращения площади (например, посредством протягивания констант, определения общих подвыражений и т.п.) или задержки (в частности, путем протягивания поздно приходящих сигналов ближе к точкам выхода) обычно производится при помощи БДР. | ||