М.С. Шуплецов - Основы проектирования цифровых интегральных схем, страница 2

Rudell, (1986-06-05), “Multiple-Valued LogicMinimization for PLA Synthesis” Memo No. UCB/ERL M86-65 (U.California Berkeley M.S. Thesis)– Giovanni DeMicheli, Synthesis and Optimization of DigitalCircuits, McGraw Hill, 1994Пример: каталоги оптимальных схемЗадача синтеза контактных схем• Пусть = 1 , … , … - счетный алфавит входныхпеременных, а 2 - множество всех функцийалгебры логики (ФАЛ) от переменных 1 , … .• Пусть К - класс (1,1)-контактных схем(КС) отпеременных из алфавита .• Сложностью Σ КС Σ ∈ К называется общеечисло контактов в этой схеме.• Сложностью () ФАЛ ∈ 2 называетсяминимальная сложность КС Σ ∈ К , реализующейФАЛ .• Функция Шеннона для сложности КС:К = max К () .∈2 ()Известные результаты в области синтезаконтактных схем от малого числа переменных• 1954-1959гг.

появились первые каталогиоптимальных и близких к ним КС для типовыхфункций от четырех переменных:– 4 ≤ 14 (Поварова Г.Н., 1954);– 4 ≤ 13 (Васильев Ю.Л., 1959).• В 1981 г. Сусов В.Ю. при помощи алгоритмовпереборного типа уточнил каталог Васильева Ю.Л.• Для функции Шеннона для сложности КС от пятипеременных известны следующие оценки:– 5 ≤ 30 (Шеннон К. Э., 1949);– 5 ≤ 28 (Поваров Г.Н., 1959);– 5 ≥ 19 (Сусов В.Ю., 1981).Инверсно-конгруэтные типы функцийалгебры логики• Инверсно-конгруэнтным типом ФАЛ будем называтьмножество ФАЛ, получаемых друг из друга при помощиприменения операций перестановки и инвертированияпеременных.• Так как операции переименования и инвертированияпеременных не меняют структуры КС, то можно считать,что КС Σ, реализующая ФАЛ , соответствуют инверсноконгруэнтному типу, которому принадлежит указаннаяФАЛ.• Множество 2∗ всех инверсно-конгруэнтных типовобразует разбиение на классы эквивалентности всехФАЛ из 2 ().• 2 5 = 4 294 967 296.• 2∗ 5 = 1 228 158.Каталог минимальных и близких к нимконтактных схем• Разработан ряд алгоритмов для оптимальныхи близких к оптимальным КС из класса К .• Используя разработанные алгоритмы, былсоставлен каталог минимальных и близких кним КС для функций от не более, чем пятипеременных.• На основе построенного каталога КС, былаполучена следующая оценка:К 5 ≤ 19.Каталог минимальных и близких к нимконтактных схемhttp://mks2.cs.msu.ru123456789124124011246117977319101112131415161727677 86624 213992 336779 311798 175207 55363 1009618198639Области применения каталоговоптимальных схем• Основа для построения библиотеклогических элементов• Системы логического синтеза на основеэквивалентных преобразований• Исследование структуры и других свойствоптимальных схемПример: проверка эквивалентности ифункциональная коррекция схем2015 CAD Contest at ICCAD• Команда: 1 студент, 2 аспиранта,1 научный руководитель• Задача «Large-Scale EquivalenceChecking and Function Correction»• Команда заняла первое место• Награждение: конференция ICCAD2015 (Austin, Texas, USA)• Две публикации по результатамисследования задачиЗадача проверки эквивалентностиСФЭ12ΣМесто дляуравнения.1 2Σ − СФЭ, реализующая системуфункций алгебры логики 1 , … , от переменных 1 , … , .53Задача проверки эквивалентностиСФЭ12ΣЛогическийсинтезМесто дляуравнения.1 2Σ − СФЭ, реализующая системуфункций алгебры логики 1 , … , от переменных 1 , … , .54Задача проверки эквивалентностиСФЭ12ΣЛогическийсинтезМесто дляуравнения.1 21Σ − СФЭ, реализующая системуфункций алгебры логики 1 , … , от переменных 1 , … , .2Σ′Место дляуравнения.1′ 2′′Σ ′ − СФЭ, получающаяся в результатеприменения алгоритмов логическогосинтеза и реализующая систему 1′ , … , ′ .55Задача проверки эквивалентностиСФЭ1212Алгоритмылогическогосинтеза изменяют структуруЛогическийΣΣ′СФЭ Σ, ноне должны изменитьсинтез её функциональность:Место дляМесто для′уравнения.уравнения.∀, = 1, … , , = .1 2Σ − СФЭ, реализующая системуфункций алгебры логики 1 , … , от переменных 1 , … , .1′ 2′′Σ ′ − СФЭ, получающаяся в результатеприменения алгоритмов логическогосинтеза и реализующая систему 1′ , … , ′ .56Задача проверки эквивалентностиСФЭ1212Алгоритмылогическогосинтеза изменяют структуруЛогическийΣΣ′СФЭ Σ, ноне должны изменитьсинтез её функциональность:Место дляМесто для′уравнения.уравнения.∀, = 1, … , , = .Задача проверки эквивалентности для СФЭ Σ и Σ′′1′ 2что′1 2заключаетсяв том, чтобы установить,′Σ − СФЭ, реализующая ∀,системуΣ′ −в результате = 1, … , ,СФЭ,= получающаяся.функций алгебры логики 1 , … , от переменных 1 , … , .применения алгоритмов логическогосинтеза и реализующая систему 1′ , … , ′ .57Задача функциональной коррекцииСФЭ12ΣЛогическийсинтезМесто дляуравнения.1 21Σ − СФЭ, реализующая системуфункций алгебры логики 1 , … , от переменных 1 , … , .2Σ′Место дляуравнения.1′ 2′′Σ ′ − СФЭ, получающаяся в результатеприменения алгоритмов логическогосинтеза и реализующая систему 1′ , … , ′ .58Задача функциональной коррекцииСФЭ12Σ ′′12Σ′Место дляИзменениеуравнения.внутрисхемы1′′ 2′′Место дляуравнения.′′Σ ′′ − СФЭ, полученная в результатеизменения спецификации в СФЭ Σ иреализующая систему 1′′ , … , ′′1′ 2′′Σ ′ − СФЭ, получающаяся в результатеприменения алгоритмов логическогосинтеза и реализующая систему 1′ , … , ′ .59Задача функциональной коррекцииСФЭ12Σ ′′ЛогическийсинтезМесто дляИзменениеуравнения.внутрисхемы1′′ 2′′1′′Σ ′′ − СФЭ, полученная в результатеизменения спецификации в СФЭ Σи реализующая систему 1′′ , … , ′′2Σ′Место дляуравнения.1′ 2′′Σ ′ − СФЭ, получающаяся в результатеприменения алгоритмов логическогосинтеза и реализующая систему 1′ , … , ′ .60Задача функциональной коррекцииСФЭ12Σ ′′ЛогическийсинтезМесто дляИзменениеуравнения.внутрисхемы1′′ 2′′1′′Σ ′′ − СФЭ, полученная в результатеизменения спецификации в СФЭ Σ иреализующая систему 1′′ , … , ′′2Σ′Место дляуравнения.1′ 2′′Σ ′ − СФЭ, получающаяся в результатеприменения алгоритмов логическогосинтеза и реализующая систему 1′ , … , ′ .61Задача функциональной коррекцииСФЭ12Σ ′′ЛогическийсинтезМесто дляИзменениеуравнения.внутрисхемы1′′ 2′′1′′Σ ′′ − СФЭ, полученная в результатеизменения спецификации в СФЭ Σ иреализующая систему 1′′ , … , ′′2Σ′′′Место дляуравнения.1′′ 2′′′′Σ ′′′ − СФЭ, получающаяся из СФЭ Σ ′ врезультате локальных замен подсхеми реализующая систему 1′′ , … , ′′ .62Задача функциональной коррекцииСФЭ1212коррекции СФЭ:′′Задача функциональнойЛогическийΣ набор пар подсхем минимальногоΣ′′′найтиразмера в Σ′синтезМесто дляМесто для′Изменениеи Σ ′′ соответственно,заменакоторыхпозволяетуравнения.уравнения.из ΣвнутриполучитьсхемыСФЭ Σ ′′′ , реализующую систему {1′′ , … , ′′ }.1′′ 2′′′′Σ ′′ − СФЭ, полученная в результатеизменения спецификации в СФЭ Σи реализующая систему 1′′ , … , ′′1′′ 2′′′′Σ ′′′ − СФЭ, получающаяся из СФЭ Σ ′ врезультате локальных замен подсхеми реализующая систему 1′′ , … , ′′ .63Множества сравнения иотождествления•••••••Множество отождествления (МО) –произвольный набор входов СФЭ 1 и 2Множество сравнения (МС) – произвольноемножество вершин СФЭ 1 и 2 , отличных отвходовМС считается эквивалентным, если оносодержит две и более вершин и указанныевершины реализуют попарно равные булевыфункцииИначе, МС считается неэквивалентнымПусть сначала заданы k МС и МО на основевзаимно-однозначного соответствия входов ивыходов СФЭ 1 и 2Множество всех МС СФЭ 1 и 2 назовемразрезающим множеством (РМ)РМ, состоящее только из эквивалентных МСназывается эквивалентнымx1 … xnx’1 … x’n∑∑1 2∑∑2 2f1…fkg1…gkМО: , ′ … ( , ′ )МС: (, ) … (, )64Формальное понятие разреза••••Разрезом ориентированного ребра = (, ) будем называть парувершин (′ , ′ ), получающуюся врезультате удаления ребра идобавления ребер (, ′ ) и (′, )Выходная вершина ′ реализует туже булеву функцию, что и вершина ,или ее отрицание (инверсныйразрез) и включается всуществующее МС или формируетновоеВходная вершина ′ помеченасимволом новой входнойпеременной и включается всуществующее или новое МОНовые ребра также могут бытьразрезаны… …… …… …uuu…ve……vu’v’vРМ = МС ∪ ⋯ ∪ МСМС′ = МС ∪ ′РМ′ = РМ\МС ∪ МС′РМ′ = РМ ∪ {′}65Конусы СФЭ•••••Вершина достижима из вершины, если в графе СФЭ существуеториентированный (, )-путь.Для вершины через обозначиммножество всех входов СФЭ, изкоторых достижима.Максимальный конус вершины – множество всехвершин из которых вершина достижима, отличных от элементовмножества - вес конусаМаксимальное дерево вершины –максимальный конус этой вершины,состоящий только из вершин,полустепень исхода которых равна 1x1...∑xi...xi+m xn...V = {xi , …, xi+m}Cw(V)wf1...fk66Задача разбиения СФЭ• Задача: вставить разрезы в исходные СФЭ 1 и 2 , которыепозволяют получить РМ с наилучшим рангом• Ранг разрезающего множество определяется следующим образом:– Эквивалентные РМ всегда имеют ранг лучше, чем ранг РМ снеэквивалентными МС.– Ранг эквивалентного РМ определяется на основе сравнениявесов максимальных конусов (в порядке убывания),порожденных вершинами МС.

Например, следующие трирешения указаны от лучшего к худшему:A: (10,8,3,3) B: (10,8,5) C: (12,1).– Ранг РМ с неэквивалентными МО определяется в результатесложения весов всех максимальных конусов всех вершин,входящих в неэквивалентные МО.67Примеры – эквивалентное РМ•••Пусть заданы СФЭ 1 и 2 , реализующие булевы функции и : = 11010001 , = 11010001 .Начальное РМ является эквивалентнымНачальный ранг (без разрезов) – (5,5).∑2∑11⊕1&РМ: 1 (o, o’)68Примеры – эквивалентное РМ••Решение с введенными разрезами, которое порождает эквивалентное РМРанг решения – (4,4,2,2,1,1).1∑ 2’∑ 1’13&⊕232РМ: 3 (o, o’)1 (f, f’)2 (g, g’)69Примеры – неэквивалентное РМ•••Пусть заданы СФЭ 1 и 2 , реализующие булевы функции и : = 11010001 , = 11101110 .Исходное РМ не является эквивалентнымНачальный ранг (без разрезов) : 5 + 5 = 10.∑2∑11⊕1&РМ: 1 (o, o’)70Примеры – неэквивалентное РМ••Решение с введенными разрезами, которое порождает РМ не являющеесяэквивалентнымРанг решения: 2 + 2 = 4.132&∑ 1’∑ 2’1352⊕454РМ: 5 (o, o’)1 (d, d’)2 (e, e’)3 (f, f’)4 (g, g’)71Общая схема решения72Экспериментальные результатыNumber ofnodesin Number ofoutputsNumberof nodesin Number ofinputsBanchmarknameTotal weight of non-equivalent compared setsut22499141387610064503826415503381919138ut41364539778169522191064521230280167985110228ut8228227265143991236 1458283426705412568296588ut965024745988648061136373618866211196672697ut115612914409146001524769576602058117212ut1399128289932805225907701136185701050522ut15991287323175721516255493562656617367ut17128256824084639590290812566589132578795ut19ut211608038528814778421322474618NA 24821951200217 48463859 3051084199749194477173663185050ut23801929470710175410093493448InitialNAAntiufeev Avtaikinaet al.,et al.,ICCAD’152016201747602173Экспериментальные результаты 1−× 100% Benchmarkname• Относительноесокращениесуммарного веса неэквивалентных МС:Relative reduction of non-equivalentcomparison sets’ weight, %ICCAD’15Antiufeevet al.,2016ut291,893,396,2ut478,484,289,65ut898,299,199.34ut986,491,894,67ut1196,298,799,89ut1395,697,898,05ut1596,798,398,85ut1797,299,099,13ut19ut21NA93,7NA99,6NA99,62ut23NANANAAvtaikina et al.,201774Студенческие соревнования• CAD Contest at ICCAD– http://cad-contest-2017.el.cycu.edu.tw/CADcontest-at-ICCAD2017/• CADathlon at ICCAD– http://www.sigda.org/programs/cadathlon• ISPD CAD Contest– http://www.ispd.cc/contests/.