Диссертация (Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов)
Описание файла
Файл "Диссертация" внутри архива находится в папке "Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов". PDF-файл из архива "Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов", который расположен в категории "". Всё это находится в предмете "технические науки" из Аспирантура и докторантура, которые можно найти в файловом архиве РТУ МИРЭА. Не смотря на прямую связь этого архива с РТУ МИРЭА, его также можно найти и в других разделах. Архив можно найти в разделе "остальное", в предмете "диссертации и авторефераты" в общих файлах, а ещё этот архив представляет собой кандидатскую диссертацию, поэтому ещё представлен в разделе всех диссертаций на соискание учёной степени кандидата технических наук.
Просмотр PDF-файла онлайн
Текст из PDF
МОСКОВСКИЙ ФИЗИКО-ТЕХНИЧЕСКИЙ ИНСТИТУТ(ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ)На правах рукописиУДК 004.78Быков Сергей АнатольевичИССЛЕДОВАНИЕ И РАЗРАБОТКА МЕТОДОВАВТОМАТИЧЕСКОГО ВЫВОДА ГЕОМЕТРИЧЕСКИХОГРАНИЧЕНИЙ С ИСПОЛЬЗОВАНИЕМДЕКЛАРАТИВНОГО ПРОГРАММИРОВАНИЯ ИФОРМАЛЬНЫХ МЕТОДОВСпециальность 05.13.11 —«Математическое и программное обеспечение вычислительных машин,комплексов и компьютерных сетей»Диссертация на соискание учёной степеникандидата технических наукНаучный руководитель:к.т.н.Рыженко Николай ВладимировичМосква — 20172ОглавлениеСтр.Список сокращений и условных обозначений .
. . . . . . . . . . . . . . .5Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6Актуальность работы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6Цель исследования . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . .9Методы исследования . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10Положения, выносимые на защиту . . . . . . . . . . . . . . . . . . . . . . 10Научная новизна . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10Практическая значимость . . . . . . . . . . . .
. . . . . . . . . . . . . . . 11Степень достоверности . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11Личный вклад . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11Апробация работы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 11Публикации . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11Глава 1. Анализ методов разработки геометрии структурныхкомпонентов . . . . . . . . . . . . . . . . . . . . . . . . . . . .1.1 Тенденции развития математических и программных средств . .1.2 Разработка программного обеспечения с использованиемдекларативного программирования и формальных методов .
. .1.3 Декларативное программирование в актуальных системахавтоматического проектирования топологий интегральных схем. . 12. . 14. . 18. . 2531.41.5Потенциальные области применения декларативногопрограммирования в системах автоматического проектированияинтегральных схем . . .
. . . . . . . . . . . . . . . . . . . . . . . . 32Постановка цели и задач исследования . . . . . . . . . . . . . . . . 36Глава 2. Математическое обеспечение вычислительного комплексаавтоматического вывода геометрических ограничений . . . .2.1 Элементы логики высказываний и теории выполнимости булевыхфункций . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . .2.1.1 DPLL алгоритм . . . . . . . . . . . . . . . . . . . . . . . .2.1.2 CDCL алгоритм . . . . . . . . . . . . . . . . . . . . . . . .2.1.3 Метод поиска стабильных моделей . . . . . . . . . . . . .2.1.4 Метод перечисления решений задачи SAT . . . . . . . .
.2.2 Элементы теории графов, используемые в работе . . . . . . . . .2.3 Задача минимизации логических функций . . . . . . . . . . . . .2.4 Выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 39........4043444648525861Глава 3. Разработка вычислительного комплекса выводагеометрических ограничений . . . . . . .
. . . . . . . . . . . . .3.1 Алгоритм вывода геометрических ограничений . . . . . . . . . . .3.2 Модель данных . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.3 Алгоритм получения разрешенных топологий . . . . . . . . . . . .3.3.1 Построение задачи SAT . . . . . . . . . . . . . . . . . . . . .3.3.2 Процедура перечисления всех разрешенных топологий . . .3.4 Поиск классов топологий .
. . . . . . . . . . . . . . . . . . . . . . .3.5 Построение компактного описания правил на границах . . . . . . .3.6 Анализ и сравнение различных вариантов ограничений на границах3.7 Выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .64646670757880848688Глава 4. Применение метода автоматического выводадополнительных геометрических ограничений . . .4.1 Оборудование и ПО . . . . . .
. . . . . . . . . . . . . .4.1.1 Технологический процесс FreePDK15 . . . . . .4.1.2 Библиотека стандартных ячеек NanGate OCL154.2 Вывод правил . . . . . . . . . . . . . . . . . . . . . . .9192939598...................................44.34.4Валидация результатов . . . .
. . . . . . . . . . . . . . . . . . . . . 99Выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101Заключение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102Литература . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 107Приложение А. Актуальные проблемы разработки нанометровыхтопологий компонентов интегральных схем . . . . . . . 1285Список сокращений и условных обозначенийАНФ — алгебраическая нормальная формаБИС — большая интегральная схемаВЫП — теория выполнимости булевых формул в теорияхДНФ — дизъюнктивная нормальная формаИС — интегральная схемаКНФ — конъюнктивная нормальная формаСБИС — сверхбольшая интегральная схемаASP — программирования стабильных моделей, Answer Set ProgrammingBDD — бинарная диаграмма решений, Binary Decision DiagramITRS — Международный план по развитию полупроводниковойтехнологииOBDD — упорядоченная бинарная диаграмма решений, Ordered BinaryDecision DiagramPOS — дизъюнктивная нормальная форма, Product–of–SumsSAT — теория выполнимости булевых формулSOP — конъюнктивная нормальная форма, Sum–of–ProductsSMT — теория выполнимости булевых формул в теорияхQBF — квантифицированная булева формула6ВведениеАктуальность работы.
Научно-технический прогресс второй половиныХХ века привел к разрыву между практическими возможностями разработанныхтехнологий изготовления и существующими методами и методологиями решениятрадиционных задач проектирования. Опережающими темпами растет сложностьпроблем, которые требуется решать промышленности. Методы и средстваснижения этой сложности являются предметом активных исследований.Сегодня природа традиционных задач оптимизации в процессе разработкикардинально изменилась с увеличением числа параметров, значения которыхнеобходимо соблюдать.
Такие проекты зачастую представляют собойсложнейшие проблемы большой размерности. Сами параметры нередко связанымежду собой множеством противоречивых требований, которые необходимовыполнить. Высокая размерность таких задач приводит к тому, что практическийинтерес представляет поиск не оптимального решения, а любого, котороесоответствует всем заданным требованиям, и в кратчайшие сроки.Одним из перспективных подходов к решению подобных задач являетсяприменение формальных методов и декларативного программирования. Врамках данного подхода разработка заключается в описании задачи в терминахпредметной области и в формулировании желаемых свойств решения, а нев написании алгоритма решения. Полученная спецификация проблемы затемиспользуется в качестве входных данных некоего универсального алгоритма.Такой подход позволяет использовать одно и то же математическое и программноеобеспечение для решения широкого круга задач — детали описания конкретнойпроблемы становятся частью входных данных.
Результатом работы данногоподхода является решение, гарантированно удовлетворяющее всем заданнымограничениям; иначе может быть сгенерировано доказательство, почему такоерешение невозможно построить. Прогресс в развитии формальных методовпозволяет решать актуальные задачи индустрии, содержащие десятки тысячпараметров и сотни тысяч ограничений.Проблема роста сложности задач разработки наблюдается и в областипроектирования микро- и наноэлектроники. Переход к актуальным иперспективным технологическим процессам сопровождается увеличением7стоимости изготовления интегральных схем (ИС), что вынуждает использоватьразличные агрессивные оптимизации для контроля стоимости конечногопродукта. Вместе с тем, жесткая конкурентная среда рынка требует сокращенияцикла проектирования и ускорения выпуска новых продуктов.Одним из способов снижения сложности процесса проектированиясверхбольших интегральных схем (СБИС) является методология проектированияна основе библиотек структурных компонентов (т.н.
библиотек стандартныхячеек). В основе этой методологии проектирования лежит использование вкачестве базовых элементов стандартных ячеек — компонентов ИС, деталифизической реализации которых скрыты за абстрактным интерфейсом.Стандартные ячейки используются при построении функциональных блоков.По мере сокращения технологических норм, возрастает сложность процессаразработки структурных компонентов и длительность цикла проектирования.Необходимость в применении агрессивных оптимизаций при проектированииИС вынуждает использовать библиотеки ячеек, содержащие большое числоэлементов. Также растет и количество самих библиотек — для разных проектовмогут потребоваться специфичные наборы компонентов.Традиционно СБИС разрабатываются по методологии «сверху-вниз»,начиная с высокоуровневого поведенческого описания в терминах функцийи алгоритмов и заканчивая детальным физическим описанием СБИС.Недостатком такого подхода является резкое увеличение стоимости ошибокпри увеличении сложности проекта.
