Диссертация (1090534)
Текст из файла
МОСКОВСКИЙ ФИЗИКО-ТЕХНИЧЕСКИЙ ИНСТИТУТ(ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ)На правах рукописиУДК 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стоимости изготовления интегральных схем (ИС), что вынуждает использоватьразличные агрессивные оптимизации для контроля стоимости конечногопродукта. Вместе с тем, жесткая конкурентная среда рынка требует сокращенияцикла проектирования и ускорения выпуска новых продуктов.Одним из способов снижения сложности процесса проектированиясверхбольших интегральных схем (СБИС) является методология проектированияна основе библиотек структурных компонентов (т.н.
библиотек стандартныхячеек). В основе этой методологии проектирования лежит использование вкачестве базовых элементов стандартных ячеек — компонентов ИС, деталифизической реализации которых скрыты за абстрактным интерфейсом.Стандартные ячейки используются при построении функциональных блоков.По мере сокращения технологических норм, возрастает сложность процессаразработки структурных компонентов и длительность цикла проектирования.Необходимость в применении агрессивных оптимизаций при проектированииИС вынуждает использовать библиотеки ячеек, содержащие большое числоэлементов. Также растет и количество самих библиотек — для разных проектовмогут потребоваться специфичные наборы компонентов.Традиционно СБИС разрабатываются по методологии «сверху-вниз»,начиная с высокоуровневого поведенческого описания в терминах функцийи алгоритмов и заканчивая детальным физическим описанием СБИС.Недостатком такого подхода является резкое увеличение стоимости ошибокпри увеличении сложности проекта.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.