📄Работа №190016
Тема: ОБНАРУЖЕНИЕ НЕИСПРАВНОСТИ ЧАСТИЧНО ПОСТРОЕННОЙ СХЕМЫ ПУТЕМ ВЫЧИСЛЕНИЯ ЧАСТИЧНЫХ ФУНКЦИЙ ЕЕ НЕРЕАЛИЗОВАННЫХ ФРАГМЕНТОВ
Тип работы
Дипломные работы, ВКР
Предмет
математика
Объем:
44 листов
Год:
2021
Просмотров:
49
4440
руб.
🛒 Купить работу
Не подходит эта работа?
Закажите новую по вашим требованиям
Узнать цену на написание
Закажите новую по вашим требованиям
Представленный материал является образцом учебного исследования, примером структуры и содержания учебного исследования по заявленной теме. Размещён исключительно в информационных и ознакомительных целях.
Workspay.ru оказывает информационные услуги по сбору, обработке и структурированию материалов в соответствии с требованиями заказчика.
Размещение материала не означает публикацию произведения впервые и не предполагает передачу исключительных авторских прав третьим лицам.
Материал не предназначен для дословной сдачи в образовательные организации и требует самостоятельной переработки с соблюдением законодательства Российской Федерации об авторском праве и принципов академической добросовестности.
Авторские права на исходные материалы принадлежат их законным правообладателям. В случае возникновения вопросов, связанных с размещённым материалом, просим направить обращение через форму обратной связи.
Настоящий учебно-методический информационный материал размещён в ознакомительных и исследовательских целях и представляет собой пример учебного исследования. Не является готовым научным трудом и требует самостоятельной переработки.
📋 Содержание
Аннотация
ВВЕДЕНИЕ 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
ВВЕДЕНИЕ 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. В качестве схемы С может использоваться спецификация или частично построенная разработчиком схема, включающая ту же самую подсхему (черный ящик).
Решение этой проблемы сводится к поиску систем частично определенных булевых функций, описывающих поведение черных ящиков.
Системы частично определенных булевых функций находятся с использованием Satisfiability (SAT) решателей вместо Quantified Boolean Function (QBF) решателей или их модификаций. Использование последних, как правило, требует более сложных вычислений. В этой работе рассматриваются черные ящики с не более чем двадцатью входами, эти ограничения используются, с тем, чтобы дополнительно сократить вычисления с применением SAT решателей. В то же время рассматриваемые ограничения дают возможность выделять в качестве черных ящиков достаточно крупные подсхемы.
Постановка задачи
Задана комбинационная схема С и подсхема (черный ящик) с множеством V внутренних полюсов, являющихся ее выходами и множеством U внутренних полюсов, являющихся входами этой подсхемы (рисунок 1). Требуется построить систему частичных функций для полюсов из множества V на множестве переменных U. В качестве схемы С может использоваться спецификация или частично построенная разработчиком схема, включающая ту же самую подсхему (черный ящик).
✅ Заключение
Рассмотрена проблема проверки частичной эквивалентности (the partial equivalence checking problem, PEC) и разработано программное для вычисления системы частично определенных булевых функций. Программное обеспечение в дальнейшем будет использоваться для решения вышеописанной проблемы. Для написания программного обеспечения было необходимо:
1. изучить алгоритм построения частично определенной функции указанного полюса от внутренних переменных, предшествующих этому полюсу
2. ознакомиться с формой представления КНФ (КНФ Цейтина)
3. изучить программную библитеку для решения задачи выполнимости булевых формул (SAT-решатель)
4. разработать архитекутуру программы. Программа, по заданным входным данным, вычисляет систему частично определенных булевых функций от внутренних переменных.
1. изучить алгоритм построения частично определенной функции указанного полюса от внутренних переменных, предшествующих этому полюсу
2. ознакомиться с формой представления КНФ (КНФ Цейтина)
3. изучить программную библитеку для решения задачи выполнимости булевых формул (SAT-решатель)
4. разработать архитекутуру программы. Программа, по заданным входным данным, вычисляет систему частично определенных булевых функций от внутренних переменных.
ИЛИ
Поиск аналога
📕 Список литературы
🖼 Скриншоты
🛒 Оформить заказ
⚡ Работу высылаем в течении 5 минут после оплаты.