Д Е Иванов - Генетический подход проверки эквивалентности последовательностных схем - страница 1

Страницы:
1  2 

УДК 681.518

ГЕНЕТИЧЕСКИЙ ПОДХОД ПРОВЕРКИ ЭКВИВАЛЕНТНОСТИ ПОСЛЕДОВАТЕЛЬНОСТНЫХ СХЕМ

Д.Е. Иванов

Under the life cycle of the development of the modern digital circuits a problem of verification of two circuits is arise. It is caused, for example, by using several optimization procedures. In this paper a genetic algorithm of solving this problem is proposed. Reported experimental results on the ISCAS-89 benchmarks confirm the efficient of the proposed algorithm.

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

Під час проектування сучасних цифрових пристроїв перед розробником часто постає проблема верифікації еквівалентності двох схем Це пов 'язано, перед усім, із використанням різноманітних оптимізуючих процедур. В даній статі запропоновано алгоритм рішення такої задачі, заснований на генетичному програмуванні. Наведено результати машинних експериментів на схемах ISCAS-89, що доводять ефективність запропонованого підходу.

Введение

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

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

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

1. Постановка задачи

В качестве модели в данной работе используются синхронные последовательностные схемы (рис.1). В данной модели схема представляется в виде комбинационного блока (в свою очередь состоящего из нескольких функциональных комбинационных блоков, КФБ) и блока памяти, который состоит из D-триггеров. Далее также будем использовать следующие обозначения: V - вектор входных сигналов; #Вх - число внешних входов схемы, размерность вектора V; Y - вектор выходных сигналов; # Вых - число внешних выходов схемы, размерность вектора Y; T - вектор состояний блока памяти; # Тр - число элементовсостояния (D-триггеров) схемы, размерность вектора T; # Эл - общее число логических вентилей в схеме.

Вектор V - упорядоченное множество двоичных значений, которое подаётся на вход цифровой схемы в определённый такт времени. Последовательность si заданной длины li -

упорядоченное   множество   из   li   векторов,   которые   подаются   на   вход   схемы в

последовательные такты времени. Обозначение  vij  говорит, что мы рассматриваем в

последовательности si вектор с номером j (j = 0,...,li -1). Через A(s) обозначим выходные

реакции схемы A при подаче на её входы последовательности s . Далее везде предполагаем, что моделирование выполняется в 3-значном алфавите [8] и работа схемы начинается из полностью неопределённого состояния.

При моделировании используется преобразование синхронной последовательностной схемы в псевдокомбинационный эквивалент с дальнейшим его итеративным моделированием в последовательные такты времени. Для такого преобразования удаляют элементы состояний. Входы элементов состояний (вектор Ti на рис.1) при этом называются

псевдовыходами, а их выходы (вектор Ti-1 на рис.1) - псевдовходами.

При таком преобразовании работа блока памяти представляется следующим образом. В момент смены тактового импульса в устройстве синхронизации (для упрощения на рисунке не представлен) происходит подача на вход схемы новых входных значений vi момента

времени i ; на псевдовходы подаются значения псевдовыходов схемы в предыдущий такт времени Ti-1 , после чего путём моделирования комбинационной части схемы для такта

времени i формируются выходные сигналы схемы Yi и сигналы псевдовыходов Ti .

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

Определение 1. Пусть заданы две цифровые последовательностью схемы A0 и A1. Будем

называть   схему    A0   исправной,   а   схему    A1   - модифицированной

(оптимизированной, неисправной). Схемы называются последовательностно эквивалентными (или просто эквивалентными), если при произвольном одинаковом начальном состоянии данных схем выходные реакции схем на произвольные входные последовательности s являются одинаковыми, т.е.

A0 = A1 <=> Vs :   A0 (s) = A1 (s).

(1)

Как было сказано выше, построенные на основании деревьев обхода алгоритмы [2,3] не в состоянии работать со схемами большой размерности. Это связано с нехваткой памяти для стеков возвратов алгоритмов обхода деревьев, что обусловлено большим числом элементов состояний в проектируемых схемах.

Однако проектировщику не обязательно иметь утвердительный ответ на вопрос об эквивалентности схем. Ему достаточно также знать, что схемы не являются эквивалентными. Поэтому задачу можно переформулировать, ориентируясь на поиск контрпримера. Определение 2. Если существует такая последовательность sk, на которой при одинаковых

начальных состояниях схемы A0 и A1 имеют различные выходные реакции,

то данные схемы не являются эквивалентными.

A0 * Ax если 3 sk : A0 (st) * Ax (sk ) (2)

Именно поиск такой последовательности будет являться целью предлагаемого алгоритма. В данной постановке задача не рассматривалась в отечественной научной литературе.

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

2. Генетический алгоритм верификации эквивалентности последовательностных схем

Как уже отмечалось ранее, авторы неоднократно применяли различные модификации генетического алгоритма к задачам технической диагностики [5-7].

Генетический алгоритм это итеративный процесс построения новой популяции (поколения) из текущей. Алгоритм заканчивает работу при выполнении одного из условий:

- либо найдена последовательность s , выходные реакции на которую схем A0 (s) и

A1 (s) различны (показана неэквивалентность схем);

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

В алгоритмах такого рода в качестве особи выступают входные последовательности,для которых заранее не известна длина (рис.2а). Длина входного вектора соответствует числу входов исследуемых схем A0 и A1. Для каждой входной последовательности sf

ставится в соответствие оценочная функция   /оц (sf),  которая показывает насколько

«хорошо» данная последовательность решает поставленную задачу. Вычисление оценочных функций особей является наиболее трудоёмкой фазой алгоритма и именно от этого зависит быстродействие всего алгоритма. Подробно вычисление оценочной функции особей описано в следующем разделе. Популяцией является набор таких последовательностей (рис.2б).

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

Подробнее генетические операции описаны в [5] и здесь не приводятся для краткости изложения.

Псевдокод генетического алгоритма построения входных последовательностей приведён ниже.

Генетический_алгоритм (Схема,  РазмерПопуляции, ЧислоИтераций) {

// подготовка начальной популяции ПостроитьНачальнуюПопуляцию(); ОценитьОсобей (НачальнаяПопуляция); НомерПопуляции=0;

Пока( не_достигнут_критерий_остановки ) {

НоваяПозиция=0;

Для( i=0 ; i<РазмерПопуляции ; {

ОперацияВыбора (РодительА, РодительБ); Если ( rand()  < Pc )

ОперацияСкрещивания(РодительА,  РодительБ, Потомок);

Если ( rand()  < Pm )

ОперацияМутации (Потомок); ДобавитьВПромежуточнуюПопуляцию (Потомок, НоваяПозиция); НоваяПозиция++;

}

ОценитьОсобей(ПромежуточнаяПопуляция); ПостроитьНовуюПопуляцию( РазмерПопуляции); НомерПопуляции++;

}

СоздатьОтчёт ();

}

Поясним назначение некоторых функций. Процедура «ОценитьОсобей» вычисляет оценочную функцию всех особей переданной ей популяции. Функция «ОперацияВыбора» на основании оценочной функции для особей текущей популяции строит их фитнесс-фукнции и производит выбор двух особей-родителей, над которым далее будут проводиться генетические операции. Функция «ПостроитьНовуюПопуляцию» обрабатывает текущую и промежуточную популяции и на их основе строит текущую популяцию следующей итерации алгоритма. В эту популяцию попадают лучшие особи из текущей популяции предыдущего шага алгоритма и промежуточной популяции. После этого промежуточная популяция уничтожается. Процедура «СоздатьОтчёт» формирует выходные статистические данные, как для пользователя программы, так и для системы моделирования и генерации тестов АСМИД-Е [9].

3. Вычисление оценочной функции.

Идеей предлагаемого алгоритма является направить поиск в пространстве решений в ту сторону, в которой выше активность верифицируемых схем A0 и Aj, а также выше различие

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

вышесказанном, в качестве меры применяются следующие показатели: активность исправной или неисправной схемы на заданной входной последовательности; число вентилей, псевдовыходов и выходов в схеме, различных в исправной и неисправной схемах. В нашем случае роль «неисправной» схемы выполняет схема, которая подверглась обработке

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

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

- n2 - число различных псевдовыходов схемы. В случае, когда различные значения в двух проверяемых схемах, ещё не достигли выходов, решающим является распространения таких отличий на псевдовыходы (триггеры) схемы. Наличие триггеров с различными значениями на определённом такте времени позволяет с большей вероятностью получить различия на внешних выходах схемы на следующем такте работы.

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

Таким образом, в общем виде значение фитнесс-функции имеет вид:

длина s'i длина st

ДЛ, Aj, st) = £ f(Aj, A0, si}) = £ (Cj* nj + C2* n2 + C3* П3), (3)

где:

c1 - c3 - нормирующие константы;

nl = ^ различие(g, A0, A1,   ), G - множество всех внешних выходов двух схем; n2 = ^ различие( g, A0, A1, sjj), Gl - множество псевдовыходов двух схем;

geGl

n3 = ^ различие^, A0, A1,   ), G2 - множество всех контрольных точек схемы. В нашем

случае мы предполагаем, что проектировщику известно поведение всей схемы, поэтому множество G 2 совпадает с множеством всех вентилей схемы.

Функция «различие^)» вычисляется на основе моделирования и определяется следующим образом:

fl, если значения сигналов на выходе блока g различны в двух

различие^, A0, Aj, stl) = \

g

схемах A0 и Aj при моделировании на входном наборе slj;

(4)

[0, в противном случае.

Псевдокод процедуры вычисления оценочной функции одиночной последовательности приведён ниже.

Вычисление оценочной функции(Схема, ВходнаяПоследовательность, Длина)

{

Фитнесс=0;

для (і=0;і<длина

{

БУ0=МоделированиеРаботыИсправнойСхемы(набор і) БУ1=МоделированиРаботьМодиф. Схемы (набор і) П!=ЧислоРазличныхВыходов (SV0,SV1); п2=ЧислоРазличныхПсевдовыходов (SV0rSV1); n3=ЧислоРазличныхВентилей; Фитнесс=Фитнесс+c1 *n1+c2*n2+ c3*n3;

}

}

Здесь SV0 и SV0 массивы, содержащие значения сигналов на всех контрольных линиях двух сравниваемых схем A0 и Aj [9].

4. Программная реализация и экспериментальные данные.

Страницы:
1  2 


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

Д Е Иванов - Взаимодействие компонент в распределённых генетических алгоритмах генерации тестов

Д Е Иванов - Генетические алгоритмы построения идентифицирущих последовательностей для цифровых схем с памятью

Д Е Иванов - Генетический алгоритм оптимизации рассеивания тепловой энергии входных тестовых последовательностей

Д Е Иванов - Генетический алгоритм построения диагностических последовательностей цифровых устройств

Д Е Иванов - Генетический подход проверки эквивалентности последовательностных схем