Аннотация
ВВЕДЕНИЕ 5
1 Постановка задачи 6
2 Основные понятия и определения 7
3 Обнаружение неисправности частично построенной схемы 10
4 КНФ Цейтина (разрешения) логической схемы 12
5 Вычисление частичных функций от внутренних переменных 14
6 Разработка архитектуры программного обеспечения 20
6.1 Используемые технологии 20
6.1.1 Язык C++ 20
6.1.2 SAT-решатель MiniSat 21
6.1.3 Внутреннее представление схемы 22
6.1.4 Система ABC 23
6.1.5 Кроссплатформенная система автоматизации сборки CMake 23
6.2 Общее описание архитектуры 24
6.3 Модуль вычисления частичных функций 25
6.4 Модуль разбора представления схемы 26
6.5 Модуль логических вентилей 26
7 Описание реализации программного обеспечения 27
7.1 В спомогательные псевдонимы 27
7.2 Модуль логических вентилей 27
7.2.1 Интерфейс логических функций (IGateFunction) 27
7.2.2 Класс логических вентилей (Gate) 28
7.3 Модуль разбора представления схемы 30
7.3.1 Интерфейс синтаксического анализатора списка соединений 30
7.3.2 Парсер списка соединений формата .BENCH 31
7.4 Модуль вычисления частичных функций 31
7.5 Вычисление систем частичных функций 39
ЗАКЛЮЧЕНИЕ 40
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ И ЛИТЕРАТУРЫ 41
ПРИЛОЖЕНИЕ А Пример представления схемы в формате .BENCH 42
ПРИЛОЖЕНИЕ Б Пример файла CMakeLists 43
Проблема проверки частичной эквивалентности (the partial equivalence checking problem, PEC) сводится к проверке возможности продолжения частичной реализации логической схемы до полной реализации, соответствующей данной спецификации. Предполагается, что некоторые части комбинационной схемы (черные ящики) еще не реализованы, но их спецификации (как части данной спецификации комбинационной схемы) известны.
Решение этой проблемы сводится к поиску систем частично определенных булевых функций, описывающих поведение черных ящиков.
Системы частично определенных булевых функций находятся с использованием Satisfiability (SAT) решателей вместо Quantified Boolean Function (QBF) решателей или их модификаций. Использование последних, как правило, требует более сложных вычислений. В этой работе рассматриваются черные ящики с не более чем двадцатью входами, эти ограничения используются, с тем, чтобы дополнительно сократить вычисления с применением SAT решателей. В то же время рассматриваемые ограничения дают возможность выделять в качестве черных ящиков достаточно крупные подсхемы.
Постановка задачи
Задана комбинационная схема С и подсхема (черный ящик) с множеством V внутренних полюсов, являющихся ее выходами и множеством U внутренних полюсов, являющихся входами этой подсхемы (рисунок 1). Требуется построить систему частичных функций для полюсов из множества V на множестве переменных U. В качестве схемы С может использоваться спецификация или частично построенная разработчиком схема, включающая ту же самую подсхему (черный ящик).
Рассмотрена проблема проверки частичной эквивалентности (the partial equivalence checking problem, PEC) и разработано программное для вычисления системы частично определенных булевых функций. Программное обеспечение в дальнейшем будет использоваться для решения вышеописанной проблемы. Для написания программного обеспечения было необходимо:
1. изучить алгоритм построения частично определенной функции указанного полюса от внутренних переменных, предшествующих этому полюсу
2. ознакомиться с формой представления КНФ (КНФ Цейтина)
3. изучить программную библитеку для решения задачи выполнимости булевых формул (SAT-решатель)
4. разработать архитекутуру программы. Программа, по заданным входным данным, вычисляет систему частично определенных булевых функций от внутренних переменных.
