Диссертация (1090534), страница 16
Текст из файла (страница 16)
3.11. Отношение симметрии относительно границы ячейки: формула (а) ипримеры топологий(б)75Рис. 3.12. Пример построеного окна с учетом отношений симметрии междуучастками топологииРис. 3.13. Пример ограничения на симметрию3.3.1 Построение задачи SATВ диссертационной работе был реализована процедура, представляющаявходные правила проектирования в виде логических выражений.
Каждомуобъекту топологии сопоставляется булева переменная: ее значение равноИстина, когда дискретный элемент топологии присутствует в заданной позиции;если ее значение Ложь, то объект отсутствует. Логические выражения,описывающие правила проектирования, возвращают значение Истина, еслитопология содержит нарушения заданных ограничений. Правило, запрещающее76топологию, представленную на Рисунке 3.6, может быть записано в видевыражения логики высказываний:R1 (x0 ,x1 ) = x0 ∧ x1(3.1)В случае, если оба объекта x0 и x1 представлены в топологии, формула(3.1) возращает значение Истина.
Данное правило, таким образом, может бытьпредставлено в виде логического вентиля И.В диссертационной работе для поиска разрешенных топологийиспользуются алгоритмы SAT. Специальные программы решатели (англ. SATsolvers), реализующие данный алгоритм, в качестве входных данных принимаютформулы в конъюнктивной нормальной форме (КНФ). Результатом работырешателя является такой набор значений входных параметров, для которогозаданная КНФ возвращает значение Истина. Любое логическое выражениеможет быть представлено в виде КНФ. Для подобного преобразования в общемслучае может потребоваться 2n дополнительных конъюнктов, где n — числопеременных.В диссертационной работе реализован метод трансляции Цейтинас использованием вспомогательных переменных (Tseitin, 1983).
В даннойработе вспомогательная переменная out соответствует выходу логическоговентиля. Несмотря на то, что полученная формула содержит больше переменных,она может быть удовлетворена теми же значениями входных параметров, чтои исходная. Таким образом, полученная КНФ формула возвращает значениеИстина тогда и только тогда, когда удовлетворено исходное выражениелогики высказываний. Длина итоговой КНФ формулы растет линейно отчисла переменных.Рассмотрим следующее выражение:P1 (x0 ,x1 ,out) = (out ∨ ¬x0 ∨ ¬x1 ) ∧ (¬out ∨ x0 ) ∧ (¬out ∨ x1 )(3.2)Таблица истинности, описывающая формулу (3.2) представлена вТаблице 1. Наборы входных значений, для которых (3.2) возвращает значениеИстина, соответствует таблице истиности формулы (3.1). Наборы входныхзначений, для которых значение переменной out равно Ложь, описывают77топологии, не содержащие нарушений правил проектирования.
В Таблице 1такие наборы отмечены жирным.Таблица 1 — Таблица истиности формулы (3.2)x0 x1 out P1x0 x1 out P11 1111 1000 0010 0101 0011 0100 1010 110Функция, описанная выделенными строками таблицы истиности, можетбыть получена из формулы (3.2) добавлением дизъюнкта единичной длины ¬out.Полученное выражение возращает значение Истина тогда и только тогда, когданабор входных значений соответствует разрешенной топологии:P1‘ (x0 ,x1 ,out) = ¬out ∧ (out ∨ ¬x0 ∨ ¬x1 ) ∧ (¬out ∨ x0 ) ∧ (¬out ∨ x1 )КНФ формула, описывающая разрешенные топологии с учетом всехзаданных ограничений, должна возвращать значение Истина для наборовзначений, удовлетворяющих всем заданными ограничениям. Такая формулапредставляет собой конъюнкцию всех выражений, соответствующих правилампроектирования:F (x0 ,x1 , .
. . , xn ) = P0‘ ∧ P1‘ ∧ . . . ∧ Pm‘(3.3)На следующем этапе реализовано построение окна, достаточно большого,чтобы вместить входные правила проектирования. Высота окна зафиксированаи равна высоте ряда стандартных ячеек. Ширина окна определяется размерамиисследуемых правил проектирования.В диссертационной работе границы ячеек интерпретируются как осисимметрий, как в горизонтальном, так и в вертикальном направлении. Инымисловами, если объект xi запрещен во всех топологиях, соответствующие емуобъекты справа и снизу от границ ячеек также должны быть запрещены.
Еслиобъект xi может появляться в топологиях, то соответствующие ему объекты такжеразрешены. Таким образом, к формуле (3.3) необходимо добавить выражение,которое возвращает значение Истина в случае, когда входящие в него переменные78имеют одинаковое значение и возвращает Ложь во всех других случаях:eq(xi ,xj ) = (xi ∨ ¬xj ) ∧ (¬xi ∨ xj )F (x0 ,x1 , .
. . , xn ) = P0‘ ∧ P1‘ ∧ . . . ∧ Pm‘ ∧ eq(xi , xj ) ∧ eq(xl , xk ) . . .(3.4)Выражение eq добавляет ограничение на равенство пары входных значений.В силу ограниченности объема автореферата далее по тексту ограничение eqопускается, но должно быть учтено при реализации обсуждаемых алгоритмов.3.3.2 Процедура перечисления всех разрешенных топологийДля поиска таких наборов входных параметров, при которых формула (3.4)удовлетворена, в диссертационной работе был реализован алгортим, основанныйна теории выполнимости булевых формул (англ.
satisfiability, SAT). За последние20 лет был совершен большой прогресс в развитии методов решения SAT задачи,позволивший решать даже сложнейшие проблемы в промышленности. SATалгоритм поволяет эффективно найти произвольный набор входных значений,удовлетворяющий заданную функцию.На базе алгоритма SAT можно построить метод перечисления всехудовлетворяющих наборов переменных, известный под названием AllSAT.Отличительной особенностью алгоритмов SAT и AllSAT является точность —они гарантированно находят все возможные решения.
В диссертационной работеиспользуется алгоритм, представленный в работе [81].ОПИСАНИЕ АЛГОРИТМАРеализованный алгоритм строит формулу в дизъюнктивной нормальнойформе (ДНФ). Каждая конъюнкция в ней описывает одну из возможныхразрешенных топологий:LL(x0 , x1 , x2 , x3 , x4 ) = ¬x0 ¬x1 ¬x2 ¬x3 ¬x4 ∨∨ ¬x0 x1 ¬x2 ¬x3 ¬x4 ∨ ¬x0 ¬x1 x2 ¬x3 ¬x4 ∨(3.5)∨ ¬x0 ¬x1 ¬x2 x3 ¬x4 ∨ ¬x0 x1 ¬x2 x3 ¬x4Соответствующие топологии показаны на Рисунке 3.14.
Каждый полученный79Рис. 3.14. Множество разрешенных топологий, полученных методом AllSATдизъюнкт обладает одним свойством — соответствующая топология, будучипоставленной встык к самой себе, образует также разрешенную топологию(Рисунок 3.15). Разные пары полученных топологий могут образовыватьРис. 3.15.
Примеры разрешенных топологий, составленных из одинаковыхэлементовкак разрешенные, так и запрещенные комбинации (Рисунок 3.16).Результатом работы данной процедуры является ДНФ формула, вкоторой каждый конъюнкт соответствует разрешенной топологии. Про каждуютопологию на данном этапе известно только одно — она образует разрешеннуютопологию при установке встык самой к себе.80а)б)Рис. 3.16. Примеры топологий, составленных из различных составных частей.Топология (а) разрешена, (б) запрещена3.4 Поиск классов топологийТопологии, полученные на этапе перечисления, не образуют нарушенийпри установке встык к самим себе.
Для построения дополнительных ограниченийна границах стандартных ячеек необходимо сгруппировать различные топологиив такие множества, что любая пара топологий одного множества не образуетзапрещенных топологий. В диссертационной работе для моделированияотношений между топологиями используются неориентированные графы.Неориентированный граф определен как G =< V,E >, в котором V— множество вершин, E — множество ребер. Вершина vi соответствует i–ой топологии. Ребро ei,j соединяет две вершины vi ,vj тогда и только тогда,когда соответствующие топологии вместе не образуют топологию, содержащуюнарушения правил проектирования. Пример графа, соответствуюшего формуле(3.5), приведен на Рисунке 3.17. Построение такого графа требует O(N 2 ) числаопераций, где N — число вершин.Граф G может включать в себя десятки тысяч вершин.
С целью сокращениятребуемых вычислительных ресурсов, в диссертационной работе применяетсяпроцедура разбиения графа на независимые компоненты. Для исходной ДНФформулы (3.5), описывающей все разрешенные топологии, может быть построенокомпактное представление с использованием методов минимизации логическихфункций. Компактное представление для формулы (3.5) выглядит следующим81образом:LLm in(x0 , x1 , x2 , x3 , x4 ) = ¬x0 ¬x1 − ¬x3 ¬x4 ∨∨ ¬x0 − ¬x2 − ¬x4(3.6)Символ “−” описывает элементы топологии, наличие или отсутствиекоторых в топологии никак не влияет на возникновение нарушений правилпроектирования. Каждый конъюнкт, таким образом, описывает семействатопологий. Для данной формулы может быть построен граф M , в которомвершины соответствуют конъюнктам формулы (3.6).
Ребра между вершинамипроводятся тогда и только тогда, когда элементы топологии в одинаковыхпозициях имеют одно и то же значение — в обоих семействах они присутствуютили отсутствуют. Если элемент одной из топологий помечен как “−”, то егозначение в другой топологии игнорируется. Для выполнения такого сравнениядвух топологий требуется O(n) операций, где n — число переменных вконъюнкте. Таким образом, для формулы (3.6) обе вершины графа M могу бытьсоединены.При таком построении, каждое ребро графа интерпретируется следующимобразом: если между двумя вершинами проведено ребро, то некоторыетопологии, входящие в каждую вершину, образуют разрешенную геометрию;если между двумя вершинами нет ребра — то ниодна из топологий, входящихв них, не образует разрешенную комбинацию.
Максимальная клика в такомграфе описывает множество топологий, некоторые из которых образуютмаксимальную клику. Обе вершины графа M для формулы (3.6) соединеныребром и, таким образом, некоторые топологии, входящие в оба семейства,образуют максимальные клики. Такое разбиение всех топологий позволяетпонизить размерность исходной задачи — вместо рассмотрения одного графа,включающего все найденные топологии, можно рассмотреть несколько графовменьшего размера. Данная процедура не оказывает влияния на итоговый результат— ниодно из возможных решений не удаляется из рассмотрения.Для добавления ребра ei,j в граф G выполняется установкасоответствующих топологий i и j встык.
Для полученной составнойтопологии выполняется проверка на соответствие правилам проектирования.Производительность процедуры проверки является критичной на данном этапе —для 104 вершин необходимо будет вполнить 108 /2 проверок. С целью повышенияпроизводительности данного этапа, процедура проверки транслируется в82программу на языке C++, которая затем компилируется в динамическуюбиблиотеку. Основная программа затем вызывает оптимизированную процедурупроверки топологий.В основе предложенного метода проверки нарушений правилпроектирования лежит трансляция заданного множества правил проектированияв виде КНФ.
Полученная формула транслируется в C++ выражение, состоящееиз операций дизъюнкции (||), конъюнкции (&&) и отрицания (!). Проверяемаятопология представляется в виде последовательности 0 и 1, хранящихся вконтейнере std::vector. Пример процедуры, выполняющей проверку наналичие нарушений правил проектировая, представлен ниже (часть исходногокода опущена):#include <assert.h>#include <vector>using Layout = std::vector<bool>;5 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]) || ...
);10return a0;};Каждый элемент вектора l соответствует определенному элементутопологии. Выражение a0 будет иметь значение true в случае, если полученнаятопология содержит нарушение правил проектирования, причем в данномконтексте точное положение этого нарушения или информация о входящих внего объектах не представляет практического интереса. Стоит отметить, что приКНФ формула, описывающая правила проектирования, может включать в себясотни переменных и тысячи конъюнкций и дизъюнкций.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
