Электронная библиотека диссертаций и авторефератов России
dslib.net
Библиотека диссертаций
Навигация
Каталог диссертаций России
Англоязычные диссертации
Диссертации бесплатно
Предстоящие защиты
Рецензии на автореферат
Отчисления авторам
Мой кабинет
Заказы: забрать, оплатить
Мой личный счет
Мой профиль
Мой авторский профиль
Подписки на рассылки



расширенный поиск

Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов Быков Сергей Анатольевич

Диссертация - 480 руб., доставка 10 минут, круглосуточно, без выходных и праздников

Автореферат - бесплатно, доставка 10 минут, круглосуточно, без выходных и праздников

Быков Сергей Анатольевич. Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов: диссертация ... кандидата Технических наук: 05.13.11 / Быков Сергей Анатольевич;[Место защиты: ФГБОУ ВО Московский технологический университет], 2017

Содержание к диссертации

Введение

Глава 1. Анализ методов разработки геометрии структурных компонентов 12

1.1 Тенденции развития математических и программных средств . 14

1.2 Разработка программного обеспечения с использованием декларативного программирования и формальных методов 18

1.3 Декларативное программирование в актуальных системах автоматического проектирования топологий интегральных схем . 25

1.4 Потенциальные области применения декларативного программирования в системах автоматического проектирования интегральных схем 32

1.5 Постановка цели и задач исследования 36

Глава 2. Математическое обеспечение вычислительного комплекса автоматического вывода геометрических ограничений 39

2.1 Элементы логики высказываний и теории выполнимости булевых функций 40

2.1.1 DPLL алгоритм 43

2.1.2 CDCL алгоритм 44

2.1.3 Метод поиска стабильных моделей 46

2.1.4 Метод перечисления решений задачи SAT 48

2.2 Элементы теории графов, используемые в работе 52

2.3 Задача минимизации логических функций 58

2.4 Выводы 61

Глава 3. Разработка вычислительного комплекса вывода геометрических ограничений 64

3.1 Алгоритм вывода геометрических ограничений 64

3.2 Модель данных 66

3.3 Алгоритм получения разрешенных топологий 70

3.3.1 Построение задачи SAT 75

3.3.2 Процедура перечисления всех разрешенных топологий . 78

3.4 Поиск классов топологий 80

3.5 Построение компактного описания правил на границах 84

3.6 Анализ и сравнение различных вариантов ограничений на границах 86

3.7 Выводы 88

Глава 4. Применение метода автоматического вывода дополнительных геометрических ограничений 91

4.1 Оборудование и ПО 92

4.1.1 Технологический процесс FreePDK15 93

4.1.2 Библиотека стандартных ячеек NanGate OCL15 95

4.2 Вывод правил 98

4.3 Валидация результатов 99

4.4 Выводы 101

Заключение 102

Литература 107

Приложение А. Актуальные проблемы разработки нанометровых топологий компонентов интегральных схем 128

Разработка программного обеспечения с использованием декларативного программирования и формальных методов

По мере роста сложности программных систем, для их разработки все чаще используются формальные методы и декларативное программирование. Эти технологии применяются для верификации распределенных систем, автоматической генерации тестов, при решении задач автоматического планирования и составления расписаний. В основе данного подхода нередко лежит использование алгоритмов семейства SAT.

Рост комплексности и сложности современных программных систем вынуждает разработчиков пользоваться различными средствами проектирования, такими как UML/OCL. Верификация и валидация таких моделей ПО и оборудования является актуальной проблемой современных средств разработки. Поведение таких моделей описывается операциями с ограничениями на начальное и конечное состояние системы. Одако, этой информации зачастую недостаточно для полного описания процесса перехода из начального состояния в конечное. Как правило, эта проблема решается описанием дополнительных ограничений. Предложены и различные методы верификации подобного описания UML/OCL моделей, основанных на символьных вычислениях. Каждому возможному состоянию системыставится в соответствие переменненая, взаимоотношения между ними и возможные переходы задаются в виде ограничений. В работе [23] рассматривается процедру верификации UML/OCL моделей с использованием алгоритма SAT, учитыващей дополнительные ограничения на переходы от одного состояния к другому.

Современное ПО все больше опирается на использование параллелизма и конкуррентности. Однако, данные технологии значительно усложняют программные системы и вносят новые классы ошибок, например, возможность возникновения состояния “гонки”, в которм несколько потоков блокируют доступ к одному и тому же ресурсу и ждут завершения друг друга. В работе [24] рассматривается метод на основе SAT алгоритма для анализа специального класса сетей Петри — сетей Гадара. Этот формализм используется для моделирования поведения многопоточных систем. SAT используется для генерации оптимальной стратегии управления многопоточным выполнением с учетом теории дискретных систем управления. Экспериментальные результаты демонстрируют высокую степень масштабируемости предложенного подхода, в сравнении с классическими методами. Эксперименты показывают, что подход с использованием алгоритма SAT позволяет генерировать системы управления для моделей с более 100 небезопасных состоянии.

Прогресс в развитии методов решения задачи SAT позволяет работать над реальными проблемами промышленности, которые могут содержать тысячи и десятки тысяч переменных. В работе [25] рассматриваются проблемы планирования и назначения. Для решения этих задач приводятся методы сведения к проблеме SAT, которые затем решаются при помощи современных алгоритмов. Эеспериментальные результаты показывают, что данный подход отличается высокой степенью масштабируемости.

Решение ряда практических задач требует от решателя поиска ответа на последовательность сходных задач. Перезапуск алгоритма с нуля приведет к полной очистке наборов выученных утверждений и частичных наборов значений. Возможность формулирования инкрементальных запросов позволяет избежать повторного вычисления уже известных данных. Существует два основных метода обеспечения инкрементальности. Один из них основан на добавлении или исключении предположений(англ. assumption). Второй способ основан на добавлении или удалении утверждений. Предположением называется конъюнкция утверждений единичной длины, которая добавляется в начало доказательства. Как следствие, для отмены предположения достаточно отменить соответствующие решения. Для невыполненных формул решатель возвращает то подмножество предположения, которое не может быть выполнено в рамках заданных ограничений. Алгоритм обучения с конфликтами естественным образом поддерживает добавление утверждений. Однако, удаление утверждений сопровождается дополнительной работой — выученные утверждения, основанные на исключенных фактах, также должны быть сброшены. В работах [26; 27] при добавлении нового утверждения создается дополнительный контекст, в рамках которого продолжается решение исходной задачи. При удалении утверждения, этот контекст сбрасывается. В работе [28] используются дополнительные литералы, которые позволяют включать или выключать заданные утверждения.

Подход с использованием предположений, впрочем, обладает двумя недостатками, которые снижают производительность всего алгоритма. Во– первых, использование предположений не позволяет выполнять предварительное упрощение заданной формулы при помощи специального препроцессора SatElite, представленного в работе [29]. Данный препроцессор активно используется при решении практических задач. Во-вторых, предположения всегда остаются в формуле, а не удаляются в ходе решение процедурой распространения констант. В литературе обсуждаются методы решения как первой проблемы [30], так и второй [31], но не обеих вместе. В работе [32] рассматривается подход, адресующий обе проблемы одновременно, в котором сначала в задачу добавляются предположения, после чего применяется алгоритм SatElite. Предложенный алгоритм демонстрирует более высокую производитесльность по сравнению с существующими подходами. В качестве экспериментальных данных использовались общедоступные тестовые примеры, полученные в ходе решения промышленных задач верификации полупроводниковых устройств.

Современные решатели рализуют сложные эвристики и оптимизации и, как следствие, могут содержать трудновоспроизводимые ошибки. Для валидации используемых алгоритмов может быть использована построенная решателем модель — выполняющего набора значений достаточно для проверки того, что заданные ограничения удовлетворены. Однако, для валидации невыполненных ограничений нужны дополнительные данные, т.к. модель в таком случае не будет построена. Для проверки результата строится доказательство противоречия, описывающее последовательность шагов резолюций. В случае неыполнимости поставленной задачи, последняя резолюция приведет к пустому утверждени. Полученный ориентированный ациклический граф представляет собой доказательство невыполнимости. Однако, данный подход повышает потребление вычислительных ресурсов в ходе решения задачи.

Расширением алгоритмов SAT являются методы решения задач выполнимости формул в теориях (англ. satisfiability modulo theories, SMT). Данный подход позволяет решать задачи выполнимости в терминах целых и вещественных чисел, теории списков и битовых векторов и др. SMT теория может включать в себя произвольные переменные, а не только булевы. Предикатами же в этой теории может быть любое булевое выражение от этих переменных. SMT теория предоставляет больше возможностей для моделирования, чем формулы SAT. Например, SMT-формула позволяет моделировать операции функции модулей микропроцессора на уровне слов, а не на уровне битов.

При разработке современного ПО большое внимание уделяется тестированию и обеспечению корректности и надежности. В работе [33] описывается программный комплекс KLEE, предоставляющий инструменты символьного выполнения программы и автоматической генерации тестов. Программная система KLEE была использована для анализа 89 программ из пакета GNU Coreutils, которые установлены на миллионах компьютеров по всему миру и тщательно протестированы. Покртыие тестами составило более 90% строчек кода, что существенно превышает покрытие тестами. написанными вручную. Также были проанализированы 75 программ пакета Busybox, для 31 из которых было достигнуто 100% покрытие кода. В общей сложности, при помощи KLEE были проанализированы 452 программы (более 430 тысяч строчек кода), в которых было обнаружено 56 критических ошибок. 3 из них не были найдены на протяжении последних 15 лет. KLEE использует SAT и SMT алгоритмы для анализа исходных кодов ПО и генерации тестов.

KLEE также используется в качестве инструмента для поиска ошибок и генерации тестов на базе документации (англ. Document-Assisted Symbolic Execution, DASE). Проект DASE. представленный в работе [34], использует методы анализа естественного языка и эвристики для обработки документации к программной системе. В результате DASE автоматически выводит ограничения на входные параметры ПО. Эта информация затем используетс для управления процессом символьного выполнения, обращая больше внимания на семантически важные участки кода. При помощи DASE были проанализированы такие пакеты программ, как foreutils, findutils, grep, binutils, elftoolchain. Было обнаружено 12 критических, прежде неизвестных и не обнаруженных другими системами символьного выполнения, 6 из них подтверждены разработчиками. Степени покрытия кода, условия и вызовов были улучшены на 14.2–120.3%, 2.3–167.7% и 16.9–135.2%, соответственно. 97.8-100% полученных ограничений корректны.

Элементы теории графов, используемые в работе

Рассмотрим неориентированный граф G = V,E , где V — множество вершин, E — множество ребер. Соседними называются две вершины, соединенные ребром. Кликой называют такое множество вершин, что любая пара соединена ребрами. Размером клики назввают число вершин, которое она включает. Максимальной назвают клику, которая не может быть расширена добавлением вершин. Степенью вершины называется число вершин, соединенных с заданной.

Известны два варианта задачи о клике. Первой можно назвать задачу “распознавания”, в рамках которой необходимо определить, содержит ли заданный граф клику размера k. Второй вариант является задачей оптимизации — в заданном графе требуется найти клику максимального размера. Задача поиска клик является NP-полной и, таким образом, эффективно алгоритма решения этой задачи пока не обнаружено. Полный перебор всех подграфов с проверкой на полноту не может быть использован на практике — число клик размером k для графа с v вершинами равняется биномиальному коэффициенту

В работе [87] рассмотрен метод ветвей–и–границ для поиска максимальной клики или, что вычислительно эквивалентно, для поиска наибольшего независимого множества. В основе метода лежит стратегия удаления лишних решений через процедуру раскраски вершин графа. Эффективность алгоритма подтверждена при решении задач для случайных графов и на DIMACS наборе графов.

Метод ветвей–и–границ используется и в работе [88] для поиска максимальных клик. Предложенный алгоритм также использует в качестве оптимизации процедуру расскраски вершин графа, в данном случае приближенную. Раскраска позволяет оценить верхнюю границу на размер максимальной клики. Также используется сортировка вершин графа для ускроения процедуры поиска. Эспериментальные результаты показывают, что предложенный алгоритм обеспечивает наилучшую производительность по отношению к другим известным алгоритмам. Метод был применен к решению практических задач в областях обработки изображений, проектировании СБИС, а также в молекулярной биологии.

Первым алгоритмом перечисления максимальных клик считается алгоритм Брона-Кербоша [89]. Его особенностью является то, что время, требуемое алгоритмом для поиска максимальных клик, зависит от их числа. Таким образом, вычислительные ресурсы, требуемые данному алгоритму, определяются не только размером входных данных, но и объемом выходных данных. В основе алгоритма лежит использование рекурсивного поиска с возвратами.

Эквивалентной задаче перечисления максимальных клик графа является задача поиска наибольших независимых множеств вершин графа. В работе [90] предложен алгоритм перечисления максимальных независимых множеств, требующий О {пищ) шагов и 0(п + т) памяти, где п, т и /І число вершин, ребер и число максимальных независимых множеств, соответственно.

В работе [91] предлагается метод перечисления максимальных клик, в основе которого лежит модифицированный алгоритм Брона-Кербоша. На первом этапе рассматриваются ребра между вершинами, которые являются кликами размера 2. Затем подклики объединяются в максимальные клики при помощи алгоритма ветвления-и-границ. Немакисмальные клики при этом опускаются, что позволяет ускорить процедуру поиска. В статье разбираются как сходства с алгоритмом Брона-Кербоша, так и различия. Приводится пример практического использования алгоритма в решении задач биохимии, а имеено в задачах анализа и визуализации метаболических процессов.

Проблема перечисления максимальных клик возникает при решении практических задач теории графов, интеллектуального анализа данных и биоинформатике. Экспоненциально растущие требования к вычислительным ресурсам известных алгоритмов перечисления ограничивают их применимость при решении актуальных задач разработки. Вместе с тем, современные проблемы нередко могут быть описаны большими графами, включающими миллионы вершин и ребер. В работе [92] предлагается параллельный алгоритм перечисления максимальных клик графа, использующий ряд новых эвристик и оптимизаций. Эксперименты с использованием графа, содержащего 2423807 вершин и 5317183 ребра демонстрируют, что данный алгоритм обладает высокой эффективностью и хорошо масштабируется для задач высокой размерности.

В работе [93] рассматривается метод перечисления всех максимальных клик графа G, который содержит п вершин и т ребер. В работе предлагается два алгоритма. Первый из них требует 0(М(п)) времени и 0(п2) памяти, второй требует 0(А4) времени и 0(п + т) памяти, где А обозначает максимальную степень графа G, М(п) обозначает время, необходимое для перемножения двух матриц размером п х п matrices. Последний алгоритм также требует 0(пт) времени для предварительной подготовки. Эксперименты показывают, что предложенные алгоритмы эффективно перечисляют максимальные клики как для плотных, так и разреженных графов, в том числе для случайных графов и графов, построенных при решении практических задач.

В основе предложенного алгоритма лежит метод обратного поиска [94]. Число шагов, требуемое алгоритму, полиномиально зависит от размера входных данных и от количества найденных в результате объектов. Требуемый объем памяти полиномиально зависит от размера входных данных. Также этот алгоритм хорошо поддается параллелизации за счет того, что ход выполнения может быть естественным образом разделен на независимые подзадачи.

Рассмотрим граф g, вершины которого соответствуют элементам множества, которе необходимо перечислить. Пусть также определена целевая функция, параметрами которой являются вершины g, и максимум которой необходимо найти. Также задана функция локального поиска, значение которой зависит от вершины графа g, которая движется по вершинам графа в направлении увеличения значения целевой функции. Данная процедура поиска должна быть детерминированной и завершаться за конечное число шагов. Вершина с наибольшей стоимостью по сравнению со смежными вершинами, назвается локальным оптимумом. Примерами такой процедуры поиска может быть симплекс метод в линейном программировании, метод обмена ребрами для поиска минимального остовного дерева в взвешенных графах, алгоритм переворота для построения триангуляции Делоне на плоскости. Стоит отметить, что симплекс метод в общем случае не является конечным, только при использовании определенных методов перехода к следующим вершинам, например, при рассмотрении метода Бланда.

Пусть граф g содержит один локальный экстремум — вершина x. Определим также ориентированный граф T, который содержит те же вершины, что и g, а множество ребер образовано упорядоченными парами вершин (x,x ), которые были полученным при выполнении процедуры локального поиска. T, таким образом, является остовным деревом с единственным стоком x. В случае, если будет выполнен обход дерева в направлении, обратном указанному ребрами, будет получена процедура, обратная локальному поиску, а он, в свою очередь, будет соответствовать поиску с возвратами. Стоит отметить, что хранить информацию о вершинах, посещенных ранее, не требуется, т.к. T является деревом.

Описанная процедура может быть использована при решении различных задач комбинаторики. Важно отметить, что любая вершина y являющаяся потомком x в дереве T, имеет меньшее значение целевой функции, чем x. Пусть стоит задача найти такую вершину в Т, которая удовлетворяет дополнительное ограничение (например, целочисленность) с наибольшим значением целевой функции. Для решения подобной задачи можно быть выполнен частичный обратный поиск. Для этого необходимо сохранить наилучшее решение х и соответствующее значение целевой функции z и в случае, если найдено решение, удовлетворяющее заданному ограничению, то сохраненные значения должны быть обновлены. Если текущая вершина обладает меньшим значением целевой функции, то нет смысла спускаться ниже по дереву.

Поиск классов топологий

Топологии, полученные на этапе перечисления, не образуют нарушений при установке встык к самим себе. Для построения дополнительных ограничений на границах стандартных ячеек необходимо сгруппировать различные топологии в такие множества, что любая пара топологий одного множества не образует запрещенных топологий. В диссертационной работе для моделирования отношений между топологиями используются неориентированные графы.

Неориентированный граф определен как G = V,E , в котором V — множество вершин, E — множество ребер. Вершина vi соответствует i– ой топологии. Ребро ei,j соединяет две вершины vi,vj тогда и только тогда, когда соответствующие топологии вместе не образуют топологию, содержащую нарушения правил проектирования. Пример графа, соответствуюшего формуле (3.5), приведен на Рисунке 3.17. Построение такого графа требует O(N2) числа операций, где N — число вершин.

Граф G может включать в себя десятки тысяч вершин. С целью сокращения требуемых вычислительных ресурсов, в диссертационной работе применяется процедура разбиения графа на независимые компоненты. Для исходной ДНФ формулы (3.5), описывающей все разрешенные топологии, может быть построено компактное представление с использованием методов минимизации логических функций. Компактное представление для формулы (3.5) выглядит следующим

Символ “—” описывает элементы топологии, наличие или отсутствие которых в топологии никак не влияет на возникновение нарушений правил проектирования. Каждый конъюнкт, таким образом, описывает семейства топологий. Для данной формулы может быть построен граф М, в котором вершины соответствуют конъюнктам формулы (3.6). Ребра между вершинами проводятся тогда и только тогда, когда элементы топологии в одинаковых позициях имеют одно и то же значение — в обоих семействах они присутствуют или отсутствуют. Если элемент одной из топологий помечен как “—”, то его значение в другой топологии игнорируется. Для выполнения такого сравнения двух топологий требуется 0(п) операций, где п — число переменных в конъюнкте. Таким образом, для формулы (3.6) обе вершины графа М могу быть соединены.

При таком построении, каждое ребро графа интерпретируется следующим образом: если между двумя вершинами проведено ребро, то некоторые топологии, входящие в каждую вершину, образуют разрешенную геометрию; если между двумя вершинами нет ребра — то ниодна из топологий, входящих в них, не образует разрешенную комбинацию. Максимальная клика в таком графе описывает множество топологий, некоторые из которых образуют максимальную клику. Обе вершины графа М для формулы (3.6) соединены ребром и, таким образом, некоторые топологии, входящие в оба семейства, образуют максимальные клики. Такое разбиение всех топологий позволяет понизить размерность исходной задачи — вместо рассмотрения одного графа, включающего все найденные топологии, можно рассмотреть несколько графов меньшего размера. Данная процедура не оказывает влияния на итоговый результат — ниодно из возможных решений не удаляется из рассмотрения.

Для добавления ребра ehJ в граф G выполняется установка соответствующих топологий і и j встык. Для полученной составной топологии выполняется проверка на соответствие правилам проектирования. Производительность процедуры проверки является критичной на данном этапе — для 104 вершин необходимо будет вполнить 108/2 проверок. С целью повышения производительности данного этапа, процедура проверки транслируется в программу на языке C++, которая затем компилируется в динамическую библиотеку. Основная программа затем вызывает оптимизированную процедуру проверки топологий.

В основе предложенного метода проверки нарушений правил проектирования лежит трансляция заданного множества правил проектирования в виде КНФ. Полученная формула транслируется в C++ выражение, состоящее из операций дизъюнкции (), конъюнкции (&&) и отрицания (!). Проверяемая топология представляется в виде последовательности 0 и 1, хранящихся в контейнере std::vector. Пример процедуры, выполняющей проверку на наличие нарушений правил проектировая, представлен ниже (часть исходного кода опущена):

#include assert.h

#include vector

using Layout = std::vector bool ;

const std::size_t maxidx = 9;

extern ”C” bool check_layout (const Layout& l);

bool check_layout (const Layout& l) {

assert (l.size() == maxidx);

const bool a0=((l[0] && l[1]) (l[3] && l[2]) ... ); 10 return a0; };

Каждый элемент вектора l соответствует определенному элементу топологии. Выражение a0 будет иметь значение true в случае, если полученная топология содержит нарушение правил проектирования, причем в данном контексте точное положение этого нарушения или информация о входящих в него объектах не представляет практического интереса. Стоит отметить, что при КНФ формула, описывающая правила проектирования, может включать в себя сотни переменных и тысячи конъюнкций и дизъюнкций. При компилировании высокооптимизированной библиотеки из исходного кода, компилятор gcc выполняет оптимизации, при которых объем занимаемой памяти квадратично зависит от длины логического выражения. Для компенсации этого эффекта КНФ формула может быть разделена на отдельные выражения:

bool check_layout (const Layout& l) { assert (l.size() == maxidx); const bool a0=((l[0] && l[1])); const bool a1=((l[3] && l[2]));

return a0 a1 ... ; };

Предложенная оптимизация позволила добиться снижения временных задержек на выполнение каждой итерации проверки нарушений правил проектирования на четыре порядка: с 10-2 сек. до 10-6 сек., по сравнению с вариантом, основанным на коммерческом программном комплексе.

Попарные отношения между разрешенные топологиями могут быть описаны кликами графа. Практический интерес представляют максимальные клики — полные подграфы, которые не могут быть расширены добавлением новых вершин. Для перечисления максимальных клик графа в диссертационной работе используется алгоритм, представленный в работе [93].

Выходными данными реализованного алгоритма является множество максимальных клик, соответствующие подмножеству конъюнкций формулы (3.5). Каждое такое подмножество описывает группу топологий, которые не создают нарушений при установке встык друг с другом. На Рисунке 3.18 представлены две максимальные клики графа, изображенного на Рисунке 3.17. Формулы (3.7) и (3.8) описывают топологии, входящие в каждую из построенных максимальных клик.

Библиотека стандартных ячеек NanGate OCL15

В работе [111] описываются различные аспекты разработки стандартных элементов в рамках перспективных технологических процессов. Предлагается библиотека стандартных ячеек, спроектированных в рамках 15 нм технологического процесса. Разработка ячеек с учетом данной технологии позволяет проиллюстрировать ряд проблем, которые не возникают при использовании предыдущих технологий. Примерами таки При разработке элементов использовалась актуальная общая модель прогнозирования технологий(англ. predictive technology model). Библиотека предназначена для использования образовательными учереждениями и исследовательскими институтами для проектирования топологий СБИС с использованием стандартных ячеек и для разработки программных систем автоматического синтеза СБИС и необходимых алгоритмов. Примером такой проблемы можно назвать необходимость в использовании метода двойного шаблона как для слоя полисиликона, так и для слоев металлизации. Также используется ряд ограничивающих правил проектирования, сокращающих вариативность топологий, что позволяет использовать технологию оптической литографии при производстве.

Данная библиотека основана на использовании FinFET транзисторов со множественными затворами, описанными в работе [112]. Переход от двух- к трехмерным транзисторам привел к появлению новых проблем при разработке, включая моделирование. FinFET были предложены в 90–ых годах в качестве одного из приемников планарных транзисторов. Преимуществом FinFET технологии в сравнении с традиционными МОП транзисторами являются меньшие токи утечки.

Ограничения технологии оптической литографии необходимо учитывать при разработке компонентов с учетом актуальных и перспективных технологий. Процесс FreePDK15 описывает различные аспекты технологии двойного шаблона при учете модели литографического процесса. Технология двойного шаблона используется на этапе литографии для изготовления элементов критических размеров. Данный подход используется для всех технологий, начиная с 32 нм, когда методы коррекции эффектов оптической близости перестали обеспечивать требуемое качество изображения. В данной библиотеке технология двойного шаблона также используется для обеспечения регулярности топологий стандартных ячеек, что повышает качество изображения при изгоовлении при помощи технологии оптической литографии.

Возрастающие требования к регулярности топологии затрудняют процесс разработки топологий элементов. Например, такие затруднения могут возникнуть в силу различий в цепях для P и N транзисторов. Для обеспечения корректности соединений, требуется добавлять отступы, в случае чего затвор контролирует один транзистор, а не пару, как обычно.

Также жесткие ограничения на регулярность вынуждают использовать дополнителньые затворы, не управлящие транзисторами. Элементы слоя полисиликона должны быть размещены на фиксированном расстоянии друг от друга. Также рядом подряд может быть размещено не более двух терминалов, но некоторые ячейки библиотеки требуют размещения большего числа терминалов. В качестве изолятора в такой ситуации также используются дополнительные затворы, не подсоединенные к транзисторам.

Для того, чтобы ячейки могли быть использованы в качестве базовых элементов, они должны обладать общими свойствами, задаваемыми библиотекой в целом. В число таких характеристик входят положения линий питания и земли, ширины слоев диффузии и кармана n–типа. Множество характеристик называют также шаблоном. На Рисунке 4.4 приведен пример топологии стандартной ячейки XOR2_X1 библиотеки OCL15. Помимо геометрического шаблона, библиотека определяет единые способ наименования элементов, доступные функции, физические и электрические требования, значения мощности. Все множество этих характеристик называют архитектурой библиотеки [113]. Подобное архитектурное описание отличает библиотеку от набора случайных ячеек.

Предложенная библиотека содержит 76 стандартных ячеек, описывающих 21 распространенные логические функции. В библиотеку входит ряд секвенциальных ячеек — синхронных и асинхронных триггеров, сканирующих триггеров. Также в библиотеку входит набор дополнительных ячеек. Большинство элементов комбинационной логики доступны и в каскадном исполнении — в вариантах от X1 до X16. Для выполнения экспериментов в рамках диссертационной работы были выбраны следующие 10 стандартных ячеек, которые наиболее активно используются при проектировании функциональных блоков: AND2_X1, AOI21_X1, BUF_X1, INV_X1, MUX2_X1, NAND2_X1, NOR2_X1, OAI21_X1, OR2_X1, XOR2_X1.