📄Работа №197587
Тема: ПОИСК УСТАНОВОЧНОЙ ПОСЛЕДОВАТЕЛЬНОСТИ ДЛЯ ПОСЛЕДОВАТЕЛЬНОСТНОЙ СХЕМЫ С ИСПОЛЬЗОВАНИЕМ SAT-РЕШАТЕЛЕЙ
Характеристики работы
Тип работы
Магистерская диссертация
Предмет
Информатика и вычислительная техника
Объем:
48 листов
Год:
2018
Просмотров:
43
4865
руб.
🛒 Купить работу
Не подходит эта работа?
Закажите новую по вашим требованиям
Узнать цену на написание
Закажите новую по вашим требованиям
Представленный материал является образцом учебного исследования, примером структуры и содержания учебного исследования по заявленной теме. Размещён исключительно в информационных и ознакомительных целях.
Workspay.ru оказывает информационные услуги по сбору, обработке и структурированию материалов в соответствии с требованиями заказчика.
Размещение материала не означает публикацию произведения впервые и не предполагает передачу исключительных авторских прав третьим лицам.
Материал не предназначен для дословной сдачи в образовательные организации и требует самостоятельной переработки с соблюдением законодательства Российской Федерации об авторском праве и принципов академической добросовестности.
Авторские права на исходные материалы принадлежат их законным правообладателям. В случае возникновения вопросов, связанных с размещённым материалом, просим направить обращение через форму обратной связи.
Настоящий учебно-методический информационный материал размещён в ознакомительных и исследовательских целях и представляет собой пример учебного исследования. Не является готовым научным трудом и требует самостоятельной переработки.
📋 Содержание
ВВЕДЕНИЕ 5
1 Постановка задачи и определение целей 6
2 Обзор существующих методов построения установочных последовательностей 9
2.1 Поиск установочной последовательности 9
2.2 Метод регулярных безусловных установочных экспериментов 10
2.3 Метод построения установочной последовательности для конечных автоматов с
помощью прямого различающего дерева 11
2.4 Задача выполнимости 12
2.4.1 Задача выполнимости булевых формул 12
2.4.2 Метод поиска кратчайшей установочной последовательности посредством
сведения к выполнимости КНФ 13
2.4.3 Оригинальный метод поиска кратчайшей установочной
последовательности 16
2.4.4 Результаты SAT Competition 2017 19
3 Алгоритмы упрощения КНФ 21
3.1 Методы, ориентированные на произвольные КНФ 21
3.1.1 Метод резолюции 21
3.1.2 Алгоритм минимизации функции component-wise quadratic (CQ) 22
3.1.3 Horn минимизация путем итеративного разложения 24
3.2 Методы, ориентированные на специфику КНФ 27
3.2.1 Идея метода упрощения КНФ разрешения 27
3.2.2 Упрощение КНФ разрешения оригинального метода 28
3.3 Выводы 28
4 Описание приложения 30
4.1 Обзор использованных технологий 30
4.1.1 Ubuntu 30
4.1.2 C Sharp 30
4.1.3 Visual Studio 2017 31
4.1.4 SAT-решатели 32
4.2 Диаграмма классов 33
4.3 Berkeley Logic Interchange Format (BLIF) 35
4.4 Построение КНФ разрешения 36
4.5 Преобразование КНФ разрешения к сертифицированному формату DIMACS CNF
37
4.6 Упрощение КНФ разрешения для блоков комбинационной логики
комбинационного эквивалента 38
4.7 Проверка на корректность установочной последовательности 42
4.8 Выводы 42
ЗАКЛЮЧЕНИЕ 45
ЛИТЕРАТУРА 47
1 Постановка задачи и определение целей 6
2 Обзор существующих методов построения установочных последовательностей 9
2.1 Поиск установочной последовательности 9
2.2 Метод регулярных безусловных установочных экспериментов 10
2.3 Метод построения установочной последовательности для конечных автоматов с
помощью прямого различающего дерева 11
2.4 Задача выполнимости 12
2.4.1 Задача выполнимости булевых формул 12
2.4.2 Метод поиска кратчайшей установочной последовательности посредством
сведения к выполнимости КНФ 13
2.4.3 Оригинальный метод поиска кратчайшей установочной
последовательности 16
2.4.4 Результаты SAT Competition 2017 19
3 Алгоритмы упрощения КНФ 21
3.1 Методы, ориентированные на произвольные КНФ 21
3.1.1 Метод резолюции 21
3.1.2 Алгоритм минимизации функции component-wise quadratic (CQ) 22
3.1.3 Horn минимизация путем итеративного разложения 24
3.2 Методы, ориентированные на специфику КНФ 27
3.2.1 Идея метода упрощения КНФ разрешения 27
3.2.2 Упрощение КНФ разрешения оригинального метода 28
3.3 Выводы 28
4 Описание приложения 30
4.1 Обзор использованных технологий 30
4.1.1 Ubuntu 30
4.1.2 C Sharp 30
4.1.3 Visual Studio 2017 31
4.1.4 SAT-решатели 32
4.2 Диаграмма классов 33
4.3 Berkeley Logic Interchange Format (BLIF) 35
4.4 Построение КНФ разрешения 36
4.5 Преобразование КНФ разрешения к сертифицированному формату DIMACS CNF
37
4.6 Упрощение КНФ разрешения для блоков комбинационной логики
комбинационного эквивалента 38
4.7 Проверка на корректность установочной последовательности 42
4.8 Выводы 42
ЗАКЛЮЧЕНИЕ 45
ЛИТЕРАТУРА 47
📖 Аннотация
В данной работе представлен метод поиска кратчайшей установочной последовательности для синхронных последовательностных схем, основанный на сведении задачи к проблеме выполнимости булевых формул (SAT) с последующим применением современных SAT-решателей. Актуальность исследования обусловлена возрастающей сложностью проектирования сверхбольших интегральных схем (СБИС) и сопутствующими трудностями их тестирования, где генерация эффективных тестовых последовательностей, включая установочные, является критически важным этапом для обеспечения надежности. Основным результатом является разработка оригинального алгоритма, который за счет специализированного упрощения конъюнктивной нормальной формы (КНФ), описывающей разрешающие условия комбинационного блока схемы, позволяет находить минимальную по длине входную последовательность, переводящую схему из неизвестного начального состояния в заданное целевое. Научная значимость работы заключается в развитии формальных методов верификации и тестирования цифровых устройств, а практическая – в создании инструментария, способного интегрироваться в промышленные потоки проектирования для повышения качества и скорости тестирования. Краткий обзор литературы охватывает классические труды по теории конечных автоматов (А. Гилл), фундаментальные исследования в области тестирования конечных автоматов (Д. Ли, М. Яннакакис), современные работы по применению ROBDD для решения схожих задач (А. Матросова и соавт.), а также специализированные исследования по поиску установочных последовательностей (Л.Д. Черемисинова), что в совокупности формирует теоретическую базу для предлагаемого подхода.
📖 Введение
Сложность проектирования сверхбольших интегральных схем (СБИС) значительно возросла за последние годы. В связи с этим усложнилась задача обеспечения правильного функционирования СБИС. Большая часть времени теперь тратится на разработку тестов, которые обеспечивают быстрое обнаружение неисправностей, возникших в процессе производства схемы.
Тестирование комбинационных схем выполняется проще чем тестирование последовательных схем с памятью, так как поведение таких схем зависит от набора состояний элементов памяти, перед подачей на входы тестовых воздействий.
Методы тестирования разделяются на встроенные и внешние. Наиболее перспективным представителем встроенного метода является Built-In Self-Test (BIST) или встроенное самотестирование. Однако при таком подходе к тестированию не все неисправности из рассматриваемого класса могут быть обнаружены, кроме того, для реализации этого подхода требуется дополнительная аппаратура. В ситуации, при которой требуется большое покрытие неисправностей тестами, используются методы внешнего тестирования. Метод внешнего тестирования основан на генерации наборов тестовой последовательности, обнаруживающей заданную неисправность. Рассматриваются синхронные логические схемы, начальное состояние которых известно. Множество тестовых наборов для заданной неисправности строится по комбинационной составляющей синхронной схемы. Обычно находятся все тестовые наборы. Тестовые наборы представляют собой полные состояния, содержащие входную составляющую и внутреннее состояние схемы. Последовательность входных векторов (установочная последовательность), переводящая схему из начального состояния в некоторое внутреннее состояние из заданного множества, представленного тестовыми наборами, является искомой тестовой последовательностью. Именно эта последовательность позволяет обнаружить заданную неисправность. В работе [1] поиск установочной последовательности сведен к операциям над ROBDD-графами, извлекаемыми из комбинационной составляющей синхронной схемы. В данной работе предлагается альтернативный подход, заключающийся в сведении к булевой выполнимости конъюнктивной нормальной формы (КНФ), строящейся для комбинационного эквивалента, состоящего из нескольких комбинационных составляющих.
Тестирование комбинационных схем выполняется проще чем тестирование последовательных схем с памятью, так как поведение таких схем зависит от набора состояний элементов памяти, перед подачей на входы тестовых воздействий.
Методы тестирования разделяются на встроенные и внешние. Наиболее перспективным представителем встроенного метода является Built-In Self-Test (BIST) или встроенное самотестирование. Однако при таком подходе к тестированию не все неисправности из рассматриваемого класса могут быть обнаружены, кроме того, для реализации этого подхода требуется дополнительная аппаратура. В ситуации, при которой требуется большое покрытие неисправностей тестами, используются методы внешнего тестирования. Метод внешнего тестирования основан на генерации наборов тестовой последовательности, обнаруживающей заданную неисправность. Рассматриваются синхронные логические схемы, начальное состояние которых известно. Множество тестовых наборов для заданной неисправности строится по комбинационной составляющей синхронной схемы. Обычно находятся все тестовые наборы. Тестовые наборы представляют собой полные состояния, содержащие входную составляющую и внутреннее состояние схемы. Последовательность входных векторов (установочная последовательность), переводящая схему из начального состояния в некоторое внутреннее состояние из заданного множества, представленного тестовыми наборами, является искомой тестовой последовательностью. Именно эта последовательность позволяет обнаружить заданную неисправность. В работе [1] поиск установочной последовательности сведен к операциям над ROBDD-графами, извлекаемыми из комбинационной составляющей синхронной схемы. В данной работе предлагается альтернативный подход, заключающийся в сведении к булевой выполнимости конъюнктивной нормальной формы (КНФ), строящейся для комбинационного эквивалента, состоящего из нескольких комбинационных составляющих.
✅ Заключение
В ходе выполнения работы был произведен обзор существующих методов построения установочных последовательностей и представлен оригинальный метод, рассмотрены несколько методов упрощения КНФ.
Методы построения установочных последовательностей:
• поиск установочной последовательности;
• метод регулярных безусловных установочных экспериментов;
• метод построения установочной последовательности для конечных автоматов с помощью прямого различающего дерева;
• метод поиска кратчайшей установочной последовательности посредством сведения к выполнимости КНФ разрешения комбинационного блока, реализующего функции возбуждения триггеров;
• оригинальный метод поиска кратчайшей установочной последовательности.
Так как необходимо найти кратчайшую установочную последовательность, то последний метод поиска удовлетворяет этому требованию.
Методы упрощения КНФ:
1. методы, ориентированные на произвольные КНФ:
• метод резолюции;
• минимизации функции CQ;
• Horn минимизация путем итеративного разложения;
2. методы, учитывающие специфику КНФ:
• метод упрощения КНФ разрешения, представленный в работе [5];
• метод упрощения, представленный в оригинальном методе поиска кратчайшей установочной последовательности.
Реализовано приложение, которое выполняет следующие операции:
• преобразование файла формата «*.blif» в нужную форму КНФ разрешения для каждого блока комбинационной логики комбинационного эквивалента, представленную в виде таблицы;
• реализация метода вывода КНФ разрешения в виде таблицы;
• упрощение КНФ разрешения;
• преобразование КНФ разрешения к сертифицированному формату DIMACS CNF;
• проверка на выполнимость с помощью SAT решателей (Riss7 или candy);
• нахождение кратчайшей установочной последовательности с помощью SAT решателя;
• проверка установочной последовательности на корректность.
Было принято участие в VI-й Молодежной научной конференции «Математическое и программное обеспечение информационных, технических и экономических систем» с докладом «Исследование и разработка алгоритмов упрощения КНФ при решении проблемы выполнимости» в рамках секции «Математическое и программное обеспечение вычислительных машин и компьютерных сетей». По окончании конференции планируется печатное издание материалов докладов в сборнике «Труды Томского государственного университета» (с постатейным размещением в базе РИНЦ), а также размещение электронного варианта издания в открытом доступе (домен «tsu.ru»).
Методы построения установочных последовательностей:
• поиск установочной последовательности;
• метод регулярных безусловных установочных экспериментов;
• метод построения установочной последовательности для конечных автоматов с помощью прямого различающего дерева;
• метод поиска кратчайшей установочной последовательности посредством сведения к выполнимости КНФ разрешения комбинационного блока, реализующего функции возбуждения триггеров;
• оригинальный метод поиска кратчайшей установочной последовательности.
Так как необходимо найти кратчайшую установочную последовательность, то последний метод поиска удовлетворяет этому требованию.
Методы упрощения КНФ:
1. методы, ориентированные на произвольные КНФ:
• метод резолюции;
• минимизации функции CQ;
• Horn минимизация путем итеративного разложения;
2. методы, учитывающие специфику КНФ:
• метод упрощения КНФ разрешения, представленный в работе [5];
• метод упрощения, представленный в оригинальном методе поиска кратчайшей установочной последовательности.
Реализовано приложение, которое выполняет следующие операции:
• преобразование файла формата «*.blif» в нужную форму КНФ разрешения для каждого блока комбинационной логики комбинационного эквивалента, представленную в виде таблицы;
• реализация метода вывода КНФ разрешения в виде таблицы;
• упрощение КНФ разрешения;
• преобразование КНФ разрешения к сертифицированному формату DIMACS CNF;
• проверка на выполнимость с помощью SAT решателей (Riss7 или candy);
• нахождение кратчайшей установочной последовательности с помощью SAT решателя;
• проверка установочной последовательности на корректность.
Было принято участие в VI-й Молодежной научной конференции «Математическое и программное обеспечение информационных, технических и экономических систем» с докладом «Исследование и разработка алгоритмов упрощения КНФ при решении проблемы выполнимости» в рамках секции «Математическое и программное обеспечение вычислительных машин и компьютерных сетей». По окончании конференции планируется печатное издание материалов докладов в сборнике «Труды Томского государственного университета» (с постатейным размещением в базе РИНЦ), а также размещение электронного варианта издания в открытом доступе (домен «tsu.ru»).
ИЛИ
Поиск аналога
📕 Список литературы
🛒 Оформить заказ
⚡ Работу высылаем в течении 5 минут после оплаты.