2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 61
Текст из файла (страница 61)
с4 С Р + Е + сз -- Н+ 10 ее„; Е + С+ сз= Л+10 сзг Ш + Л +с~ Е+1Оьсз1. И + Н + 0= Н'+!Оеср кода якой иепро. вена нно- !ШИ прн Дожжнишльно следует формализовать следующее ограничение: значения всех указанных выше семи букв должны быль различными. Поскольку свои возмакные значения буквм принимают из конечного множестве 10 цифр, мшкно кюкдую букву ззкодироввть четырьмя двоичными переменными. Кжкдый ю четырех переносов с, является двоичной переменной. Таким обрюом, всего для решения задачи нужно 32 двоичных переменных.
Конъюнкция всех ограничений, записанных квк логические функции от этик переменных, даст функцию Г, принимающую еднннчнме значения ив тех наборах двоичных переменных, которые являются ришениямн задачи. Если функция Г невыполнима, решений у звдвчи нет. Опыт показывает, что манипулирование двоичными функциямн, представленными в форме ВПП, не вызывжт затруднений, люке если зги функции зависят от нескольких десяпюв и дшке сотен двоичныл.переменных. Необхо. Рима В Бим( димые операции с функциямн, представленными в В00, вкшочеиы во все укаэанные выше библшпеки, 9.7. Использование В00 в анализе и синтезе логических схем Современные ннтегрввьные схемм содержат многие миллионы транзисторов, и их проверке, тестирование и анализ представляют чрезвычайно трудную проблему.
Если для таких схем построены В00 реализуемых схемами функций. задачи эти существенно упрощаютсл. В наспжщее время В00 являются основными струкгурами данныщ используемыми в САПР СБИС, манипуляции с В00 включены ао многие промышленные системы автоматизированного проектирования интегральных схем. Некоторме авторы монографий ло разработке интегральных схем пишут, что "В00 — зто структура да шых е области аетоматизвроеанлой разработки ИС, кашорза лримеяяемсл также н е другш облшяшэ — настолько широко и интенсивно используется этв форма прелставлення булевых функций в автоматизированном проектировании схем.
Поскольку В00 залают булевы функции, реализуемые логическими схемами, нх можно считать представлением логических схем. Если схема ревяизуег несколько логических функций, имеющих общие псцсхемы, то многовыходную схему моюю представить В00 с несколькимн головными вершинами, шиклвя нз которых предспшляет евою схему. Такие В00 называются резделлемыми (зйшвд). Рнс. 9.20 представляет пример разделяемой В00 с двумя двоичнымн входами и тремя выходами.
Фактически, разделяемая В00 представляет совместную минимизацюо нескольких булевых функций в базисе (О, 1, «я~ при заданном порядке переменных. Некоторьш обяасти применении В00 в САПР СБИС следующие: логический сюггез, верифшшцня, генерация тестов, молелированне отказов (бзн)г мпшЫюл). Логический синтез — ревлнзвции схемы не ВВЭ. Самый простой и прямой метод реализации лснмческой схемы по представленшо соответствующей функции в В00 — это использование мультиплексора (МСХ) — схемы, имеющей несколько входоа н один выход.
МУХ реализует функцию «е(х, у, з)=(г хгйялуе(тез ст трех двоичных переменных. Рис.921 показывает техмику такой ревлмнщни. Из этого примера видно, что графнчешщ д гщ иеВ00од в о жщ у у юеа р о все х У ЛеКНх1 як Лзеп у ыее а який (рвай пряную. .емы, )унк- 9.21 зине вьтн- оров, аную уункются пуля- оаан~й по зллсе я зта рова.
сами, нзует зхолзами, азде,вумя трел- юисе Рпс. 929. В00 трех булевых функций: А лВ у, Л= . л у. ДФ*лм у б Рие.9.21. Непосрелственюм реализация схемы по В00; е) мммсит МОХ. реалюующнй функцию йе(х, у, я); 6) соетвеытвне фрагмента В00 и схемы МНХ мзе коз тси с РТ1. ( Развнз банан Анааз функн схемы функи ных сз лов к ыо фу ск3но! Рзы.Р.З!. йеоосрелсзвенннз реаанзашы схемы но ВОЮ: о) Реавнзвым схемы оо В01у плексоров, реализующей функцию. В настоящее время зто ивпраымиие сиитеза схем интенсивно рювиежтая, в частности, разрабатывается технология РТЬ (Разз Тщпмзюг гойю) построения интегральных схем на основе МОХ.
Рвзвиввегся тмске так называемое направление ИЮ-йиео' уулгйез!з в комбинации РП. с СМОБ-логикой. Апалпз схемы — вмтрееиие ВВВ ие лепзчаскей схеме. Построение В00. функции, реализуемой логической схемой, осуществляется по структуре втой схемы очень просто. На рис.9.22 эю показано дяя схемы, реализующей функцию з 'зачЬ)л(ачсу. Сначала строятся В00 всех входных переменных схемы. На рис.
922 зто переменные а. Ь и с. Ъпем по ярусам, от входов к выходу стровтся В00 всех промежуточных подфункций. На рис. 9.22 зто функции х=ачЬ, у =ачс. Результирующая В00 представлястлогическую функцию з, реализуемую схемой. Рие.ФЛЗ. Нссгроеиве В00 по лопнесхой схеме Гияса Р Вернфикацва схемы: нреверка тоге, улоилетиорист лв легичесиаа схема ее специфнкациж Спецификация логической схемы обычно задается булевой формулой или наборами значений аргументов, на которых функция доюкна быть рзина 1.
По этой спецификации может быть построена ВР0 соответствующей логической функции, а по схеме можно построить В00 той функции, которая реализуется этой схемой. Сравнение двух В00 — канонических предстаалений этих двух булевых функций — позяоляеглегко прав. рить, удовлетворяет ли схема ее спецификации.
Проверка экиииалевтиости двух логических схем. Одну и ту жс булеау функцию могут реализовывать различные логические схемы (они, конечно, дожкны иметь одинаковое число двоичных входов н одинаковое число дао. ичных выходов). Проверка экаиааленпюсти логических схем мажет быть выполнена проверкой эквивалентности булевых функций, реализуемых этими схемамн. Другой способ — это построение функции г, которы равна 1 при нссоайадении значений хотя бы на одном выходе этих двух схем (рис. 9.23).
Эга проблема, фактически, проблема БАТ, решаекя построением ВР0 для логической функции, реалюующей выход схемы рис. 9.23, б, и проверкой того, существует ли у В00 этой функции терминальнаа вершина 1. Как бь сущесз к рели лучили сания относя. злемен шая об пенью'. дчйг Примо Пуст лаоичнь лс Пу т д=(а,, из А,та рис.9.2)ь а. Проверка эшаявмнпюстн двух жннческнх схем т! улеву гечно, з две. быль с эти- овйа- ~ про. гичеэ, су- схема буленкпия Ю со- 1У тол ~нони- зроее Рис. В.23, 6. Проверка эквиеаяеагнссти двух логических схем ' 9.8. Конвчныв структуры данных и В00 Как было показано выше, В1Ю уаышно используются во многих облавны, существенно расширяя гранины возможного применения булевых фучнший к решению практических задач.
Но наиболее ширшсое применение ВО1У получили в разработке эффективных алгоритмов для предспшяения н оперирования конечными структурамн данных. К таким структурам в математике относят множества и отношения. Характеристическая функинл мншкества. Пусть Я вЂ” конечное множество из ж элементов. Выберем натуральное 0=»!о02(ш)1 н закодируем все элементы Я векторами двоичных переменных яг,...,хя двиной Ф. Не уменьшая общности, можно счизать, что мощность множества Я явлштся сте. пенью 2. Пример 9.9 Пусть о состоит нз Зэлементов: (ас,а1,...,аг». Звколнруем элеишпы 8 двоичными кодами произвольнмм обрвюм, например, так (я = 3): аз сэ 000,а~ еэ 001,...,ог со111.
Пусть А — некоторое оодмноамство множеспяз Я, А а 8; напфимер, А (ас,аназ,ая». НабоР лвончных кодов, 'соответствующих элементам нз А, таков: (000,001,010,110». Обозначим Б„булску функцию, которая рвана 1 на наборах, коднрующих элементы нз. А. Дая примера 9.6 функция д„равна 1 на наборах 1000,001, 010, 110~ и рвана 0 нв всех остальных наборах. Подобнмм образом любое подмножество конечного мншкссчвв может быль задано с помощью булевой функции.
Зта функция называется характеристической функцией множества. + Оп 0.6 ичесвап мис!Вэспгеа) Характеристической функцией множества А, подмножества некоторого конечного мнояиства 8, называется булева функция, принимающая значения 1 в точности на тех двоичных наборах, которыми закодированы элементы А прн некотором фиксированном кодировании элеменгов мшхкестеа Я.
ИД! шым! Пулы П по 19 пу Унар! Гу до! Бина! П пс! Характеристическую функцию множества, как и любую булеву функцию, можно предсташпь в различных формах. Иапрнмер, таблицей истмнности, логической формулой ияи ее бинарной решвкиней диаграммой, Функция у,, примера 9.9 мгхкст быть задана таблицей истинности рис. 9.1, а, или двоич- ным решающим деревом рис. 9Л, б, или любой логической формулой приме- ра 9.3, илн бинарной решмощей диаграммой рис. 9.2. Именно предстваление харакшристических функпий мншкеств а форме ВРР оказалось очень эффективным как ляя хранения множеств, так и для выпол- нения операций над мнохмствами.
Пусть х!, хз, х! — дВОичнью персменнью, ксторьгс яаляюгся Всцомогвтсяьными, вновь введенными символами. Тогда булеаа функция! Х,! Х! Х2 ЪТЗ М Х! Х2ХЗ Ч Т! Х2 Хз МХ! Х2 Хэ щшют мнохмсгво А 1ас,а!,Сз,аь~. Итак, подмножесша конечного множества мшкно задавать логической фор. мулой, представляющей характеристическую функцию, Будем писать А = (000, 001.
010, 110Их!.хз,хз), чюбы показать закодированные эяементы мншкества А, переменные коди- ровки и их порядок Операции нцд мпмкестаамн. Все операции нвд конечными множеспщмн могут быть определены через булевы операции шщ соотвсвствующими ха- рвкшрнстическими булевыми функциями. Пусть Я вЂ” жнмчное мнакество, а Р и д — сто пцпмнакествк рассмотрим, как операции над множествами Р Такиь вы оп рнстн вы оп~ ПРВ2 С ПО Прим Пусть НОСТИ ных р сс с»' левой Бинар д ((, шсние нами ! соотве Первы ребро, и Д мОжнО Выполнить с номошь30 Операций нвд харвктергюзнческнмн фузззь низин эрих множеств ХР н Х0. Нульарные операции (константы): 12 полное ышлкество Я: зших мзои ушью :цией Х -1(ТР ); Хи 0(РО1ге).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
