д Е Иванов, Р Зуауи - Верификация эквивалентности цифровых схем с использованием стратегии симуляции отжига - страница 1

Страницы:
1  2 

УДК 681.518

© 2009 г. 1Д.Е. Иванов, 2Р. Зуауи

ІИнститут прикладной математики и механики НАН Украины, Донецк 2Донецкий национальный технический университет, Донецк

ВЕРИФИКАЦИЯ ЭКВИВАЛЕНТНОСТИ ЦИФРОВЫХ СХЕМ С ИСПОЛЬЗОВАНИЕМ СТРАТЕГИИ СИМУЛЯЦИИ ОТЖИГА

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

In this paper new algorithm for the verification of the equivalence of the sequential digital circuits is proposed. It is based on the new evolutionary strategy of the simulating annealing. This approach uses an iterative improvement of the properties of the one input sequence. Fault-free simulation of the digital circuits is used for the estimating the quality of the potential solutions. The effectiveness of the proposed algorithm is shown by its approbation on the ISCAS-89 benchmarks.

1. Введение

Разработка цифровых схем является слож­ным итеративным процессом. На каждой ите­рации схема проходит ряд преобразований как между уровнями представления (функциональ­ный, логический и т.д.), так и внутри одного уровня, когда происходит оптимизация различ­ных параметров: число логических вентилей, рассеиваемая тепловая энергия и т.п. При та­ких преобразованиях необходимо следить за тем, чтобы не изменилось эталонное функцио­нирование схемы. Это достигается путём срав­нения поведения начальной и преобразованной схем. Таким образом, задача проверки эквива­лентности является актуальной в жизненном цикле разработки последовательностных циф­ровых схем.

Построение входных последовательностей с различными диагностическими свойствами яв­ляется предметом изучения не одной группы авторов. При этом разработан целый ряд под­ходов для решения задач подобного типа. Для комбинационных и небольших последователь-ностных схем хорошо подходят методы, осно­ванные на построении деревьев обходов [1]. К сожалению, с увеличением проектируемых схем резко падает их эффективность, что связа­но с экспоненциальным ростом размера таких деревьев и, как следствие, приводит к перепол­нению стеков возвратов поисковых процедур. Ко второй группе относятся методы, основан­ные на символьном преобразовании представ­ления обрабатываемых схем [2]. Практическое применение данных алгоритмов также ограни­чено схемами небольшой и средней размерно­сти из-за аналогичных ограничений. Третья группа методов [3] преодолевает эти недостат­ки, поскольку берёт необходимую для построе­ния последовательностей информацию непо­средственно из процедур моделирования. По­скольку задача моделирования решена для больших схем (в том числе последовательност-ных) [4], то и практическое применение данных алгоритмов шире. К данной группе, в частно­сти, относятся подходы, основанные на генети­ческих алгоритмах [5-6].

Авторы также уделяли огромное внимание эволюционной стратегии генетических алго­ритмов. На её основе разработан ряд алгорит­мов построения идентифицирующих последо­вательностей: тестовых [7], инициализирую­щих [8] и верифицирующих эквивалентность двух заданных схем [9]. Однако вне внимания осталась другая эволюционная оптимизирую­щая стратегия - симуляции отжига [10]. Её ко­ренное отличие от генетических алгоритмов за­ключается в том, что здесь происходит эволю­ция только одного потенциального решения. В связи с этим отпадает механизм обработки по­пуляций, который является существенной ча­стью генетических алгоритмов. Таким образом, открывается возможность построения принци­пиально более простых алгоритмов идентифи­кации цифровых схем, которые используют стратегию симуляции отжига. Под упрощением построения алгоритмов также понимается вся связанная с их программной реализацией часть: кодирование и отладка.

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

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

2. Стратегия симуляции отжига

Стратегия симуляции отжига впервые раз­работана Метрополисом (Metropolis N.) в [10] на заре численных компьютерных эксперимен­тов. Она предложена для статистической зада­чи нахождения состояния группы атомов при остывании нагретого слитка металла. И лишь спустя три десятилетия Кирпатрик (Kirpatrick S.) в [11] применил аналогичный подход к за­дачам дискретной оптимизации, в частности, к задаче трассировки печатных плат. Таким обра­зом, в данной статье было показано, что дан­ный подход является оптимизирующей страте­гией в широком смысле. Практически одно­временно появилась статья Керни (Cerny V.) [12], показывающая применение стратегии к решению задачи коммивояжера. С тех пор ин­терес к данной стратегии неукоснительно рас­тёт и множится число её применений к практи­ческим задачам.

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

Введём некоторые базовые понятия, кото­рые необходимы для описания стратегии симу­ляции отжига. Данная стратегия представляет собой итеративный алгоритм улучшения свойств некоторого потенциального решения -конфигурации, которое для шага i алгоритма обозначается Ki. Таким образом, конфигура­ция Ki есть закодированное потенциальное решение задачи в пространстве поиска. С каж­дой конфигурацией Ki соотносится функция, которая показывает качество данной точки с точки зрения решения задачи, и называется функцией стоимости: Q = C(Ki). Также до­полнительно вводятся возмущающие операции, которые позволяют для точки Ki строить ок­ружение - некоторое множество точек с изме­нёнными характеристиками. Вычисление функций оценки для точек из окружения может показать, что их качество ухудшилось по срав­нению с исходной точкой. Принимать такие ухудшения или отклонять показывает распре­деление температур {T}. Смысл построения данного распределения заключается в том, что при больших температурах вероятность при­нять худшие решения выше, чем при более низких. Выбор распределения температур {T} показывает скорость остывания субстанции и, таким образом, существенно влияет результаты поиска.

Дадим словесное описание алгоритма симу­ляции отжига.кі+\ =

1. Алгоритм начинает работу с построения начальной конфигурации Ki = K\ и её оценки

C\ = C(K\). Также для выбранного распреде­ления температур выбирается начальная Ti = T\. Следующие шаги алгоритма повторя­ются итеративно вплоть до нахождения реше­ния на одном из них, либо до достижения верх­ней границы числа итераций.

2. Для текущей температуры Ті путём применения модифицирующих операций к те­кущей конфигурации Ki строится её окруже­ние, состоящее из N конфигураций: On = O( Kt) = {K\, k2,..., KN }

3. Для каждой конфигурации Kf из окру­жения Of вычисляется её оценка C- = C(K- ), а также параметр улучшения оценки AC- = C- -Ci, на основании которого проис­ходит/не происходит замещение текущей кон­фигурации Ki:

'К/ , если AC/ < 0;

<! К/ с вероятностью

P = exp(-AC/ / кТг), если AC/ > 0;

Изменяется счётчик итераций i = i + \, а также в соответствии с выбранным распределением температур изменяется текущая температура: Ті+\ = обновить ).

4. Переход к шагу 2.

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

3. Алгоритм верификации эквивалентно­сти и экспериментальные данные

Сформулируем более формально постановку задачи верификации эквивалентности двух за­данных схем.

Определение 1. Пусть заданы две цифровые последовательностью схемы Ao и A\. Будем называть схему Ao исправной, а схему A\ - мо­дифицированной (оптимизированной, неис­правной). Тогда схемы называются последова-тельностно эквивалентными (или просто экви­валентными), если при произвольном одинако­вом начальном состоянии выходные реакции данных схем на произвольные входные после­довательности s являются одинаковыми, т.е. A0 = A\ <=> Vs :   Ao(s) = A\(s).

При этом, исходя из практического смысла, считается, что схема A\ получена в результате некоторой оптимизации внутренней структуры схемы Ao . Другими словами структура их эле­ментов состояний одинакова, тогда как логиче­ские структуры, описывающие комбинацион­ные блоки, различны.

Задача теоретического доказательства экви­валентности схем в такой постановке является очень трудной, а для практически проектируе­мых схем невыполнимой. Однако разработчику часто нет необходимости знать, что схемы эк­вивалентны. Для оценки правильности этапа оптимизации ему достаточно знать, что схемы являются неэквивалентными, т. е. в процессе оптимизации произошёл сбой.

Поэтому, данную задачу построения вход­ных последовательностей, как и другие, кото­рые основаны на недетерминированных подхо­дах, возможно переформулировать. Для этого изменим её на противоположную: мы не будем доказывать эквивалентность заданных схем, а будем строить последовательность, которая бу­дет стараться различить их поведение. Таким образом, алгоритм будет показывать неэквива­лентность двух схем. Сформулируем задачу в такой постановке.

Определение 2. Если существует такая по­следовательность sk , на которой при одинако­вых начальных состояниях схемы Ao и A\ имеют различные выходные реакции, то дан­ные схемы не являются эквивалентными.

А * a\ если 3 sk: Ao(sk) * A\(sk)

Алгоритм симуляции отжига для решения задачи верификации эквивалентности последовательностных схем строится на основании общего алгоритма (раздел 2) путём определения его компонент: кодирование конфигураций, определения операций возмущения и вероятностей их применения,роятностей их применения, построения после­довательности температур и на его основе рас­пределения принятия отрицательных решений. Авторы уже описывали подобный алгоритм симуляции отжига, который строил инициали­зирующие последовательности последователь-ностных схем [13]. Предлагаемый алгоритм очень схож с описанным, поэтому мы дадим только его краткое описание, больше внимания уделив численным экспериментам и его опти­мизации.

В качестве модели алгоритм использует синхронные последовательностные схемы с дальнейшим их преобразованием в псевдоком­бинационный эквивалент [\4].

В описываемом алгоритме в качестве кон­фигурации выступает двоичная входная после­довательность Ki =   , для которой заранее не

известна оптимальная длина. Ширина входной последовательности равна числу внешних вхо­дов рассматриваемых схем. Кодирование кон­фигураций соответствует кодированию особей в ГА построения тестов [7].

Функция оценки традиционно для алгорит­мов данного типа строится на основании ре­зультатов моделирования. Поскольку цель ал­горитма - построить последовательность, кото­рая должна показать различие в функциониро­вании схем, то оценка должна основываться на различии поведения внутри сравниваемых схем.

Общий вид функции оценки для конфигура­ции Kj = Sj и двух заданных схем A) и A\:

длина Sj

C (К,) = f (Ao, A\, s,) = £ f (A\, Ao, sl}) =

j=\

длина Sj j=\

где C\ - C3 - некоторые нормирующие констан­ты, n\ - число различий на внешних выходах сравниваемых схем, «2 - число различий на псевдовыходах схем (элементах состояний), «3

- число различий на множестве контрольных точек. Подробно построение данной функции оценки описано в [9].

Значения эвристических параметров, напри­мер, расписание температур, подбираются экс­периментальным путём.

Сконструированный таким образом алго­ритм построения входных последовательностей реализован программно в среде программиро­вания CodeGear (студенческая версия). Объём программного кода составил около \2oo строк, включая событийный алгоритм исправного мо­делирования работы последовательностных схем.

Для проведения машинных экспериментов с программной реализацией выбрана стратегия, схожая с [9]. Для проверки эффективности ал­горитма следует проводить эксперименты на схемах, в которых произведены минимальные изменения. Причём считается, что последова-тельностная структура (структура элементов состояний) является одинаковой в сравнивае­мых схемах. А различными являются комбина­ционные блоки, реализующие функции состоя­ний и переходов. Для того, чтобы усложнить работу алгоритма, мы будем вносить некоторые миноритарные изменения. При построении двух последовательностных схем с очень близ­кой логической структурой мы пользовались следующими умозаключениями. Оптимизатор вносит изменения в некоторый логический блок. Чем меньше этот блок, тем меньше раз­личия в схемах и тем труднее построить разли­чающую последовательность. Минимальным логическим блоком, в котором можно произве­сти изменения, для вентильного уровня пред­ставления является логический элемент. По­этому схема для сравнения будет строиться из оригинальной путём случайного изменения од­ного типа вентиля в схеме. Для двух получен­ных таким образом схем мы производим запуск алгоритма верификации.

Апробация реализации алгоритма проводи­лась на схемах из международного каталога ISCAS-89 [15]. Данный каталог содержит опи­сания цифровых последовательностных схем различной размерности (от единиц до десятков тысяч вентилей) и различной сложности. На схемах данного каталога принято проводить апробацию эффективности алгоритмов иден­тификации последовательностных схем.

С целью изучения свойств алгоритма решать поставленную задачу для каждой из контроль­ных схем проводилось по 25 экспериментов.

Значения эвристических параметров, подоб­ранные на основании машинных эксперимен­тов: Тнач = \2o , Ткон = \ , шаг изменения темпе­ратуры AT = \, мощность окружения N = 5o ,

константа Больцмана k = \*\o 5, число итера­ций без улучшения оценки Nu    = 5o .

Табл.1. Результаты численных экспериментов.

название

число вентилей /

эксперименты

схемы

триггеров в схеме

всего

различено

не различено

ответ под

 

 

 

схем

схем

вопросом

s298

145 / 14

25

25

0

0

s344

198 / 15

25

25

0

0

s349

199 / 15

25

25

0

0

s382

191 / 21

25

23

1

1

s386

182 / 6

25

25

0

0

s967

465 / 29

25

21

4

0

s1196

578 / 18

25

25

0

0

s1238

557 / 18

25

25

0

0

s1423

756 / 74

25

25

0

0

s1488

689 / 6

25

23

0

2

s1494

683 / 6

25

23

0

2

s3271

1731 / 116

25

25

0

0

s3330

Страницы:
1  2 


Похожие статьи

Д Е Иванов, Р Зуауи - Алгоритм симуляции отжига оптимизации рассеивания тепла диагностических тестов

Д Е Иванов, Р Зуауи - Алгоритм симуляции отжига построения тестов цифровых устройств

д Е Иванов, Р Зуауи - Верификация эквивалентности цифровых схем с использованием стратегии симуляции отжига

Д Е Иванов, Р Зуауи - Применение стратегии симуляции отжига для построения инициализирующих последовательностей цифровых схем

Д Е Иванов, Р Зуауи - Построение идентифицирующих последовательностей цифровых схем с использованием стратеги симуляции отжига