автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.13, диссертация на тему:Верификация проектов аппаратных средств ЭВМ на основе модели взаимодействующих последовательных процессов

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ЭЛЕКТРОТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ имени В.И.УЛЬЯНОВА (ЛЕНИНА)

На правах рукописи

АЛИ АБДУЛ АМИР МОХАММАД

ВЕРИФИКАЦИЯ ПРОЕКТОВ АППАРАТНЫХ СРЕДСТВ ЭВМ НА' ОСНОВЕ МОДЕЛИ ВЗАИМОДЕЙСТВУЮЩИХ ПОСЛЕДОВАТЕЛЬНЫХ ПРОЦЕССОВ

Специальность: 05.13. .13 - Вычислительные машины,

комплексы, системы и сеты

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических.наун

Санкт-Петербург - 1994

Работа выполнена в Санкт-Петербургской государственном электротехническом университете имени В.И.Ульянова (Ленина).

Научный руководитель -

кандидат технических наук доцент Хохловский В.Н.

Официальные оппоненты:

доктор технических наук Микони C.B.

кандидат технических наук доцент Татаринов Ю. С.

Ведущая организация - АО "Светлана-микроэлектроника"

Защита диссертации состоится Я* I' О £>-------1994 р.

в |б.Об часов на заседании специализированного совета Й 063.36.12 Санкт-Петербургского государственного электротехнического университета "имени В.И.Ульянова (Ленина) по адресу: 197376, Санкт-Петербург, ул. Проф. Попова., 5.

С диссертацией можно ознакомиться в библиотеке университета

Автореферат .разослан

"ОТ " об 1994 г.

Ученый секретарь слецааяизированного совета

Балакин В.Н

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

В. настоящее.время существует три основных подхода к решению задачи проектирования аппаратных средств и доказательства их корректности:

- автоматический синтез;

- проектирование и проверка- корректности функционирования с помощью тестирования ее программной модели:

- формальное! доказательство того, что проект соответствует его функциональной.спецификации;

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

Второй подход, заключающийся в тестировании модели проектируемых аппаратных средств, является наиболее распространенным в настоящее время. Однако практически данный подход не может обеспечить доказательство полной правильности про-

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

Поэтому в последние годы было выполнено довольно много работ в' направлении создания и изучения различных теоретических моделей, методов доказательства и алгоритмов для проведения формальной верификации - проверки корректности проектов аппаратных средств ЭВМ. Естественно, что вначале методы верификации аппаратных средств были построены на основе методов верификации программ - это та область, в которой исследования начались раньше. Однако область верификации аппаратных средств имеет свои . специфические че^рты. которые должны быть отражены в создаваемых моделях. Одной из сймых важных черт является параллельное функционирование компонентов дафровых схем.

Модель взаимодействующих последовательных процессов CSP представляет собой модель работы параллельных систем. Процессы в CSP развиваются параллельно и взаимодействуют.. ..как между собой, так и с окружением, то есть CSP включает модель параллелизма с передачей сообщений. Таким образом, CSP удовлетворяет основному требсванию, заданному областью верификации проектов аппаратных средств ЭВК'- .

VHDL - язык описания аппаратуры сверхскоростных ИС является перспективным стандартом в области языков описания аппаратуры. Разработка этого языка вызвана тем, что до недавнего времени не существовало стандартного языка описания аппаратуры. Сведений об исчерпывающих средствах (как теоретических методах, так и практически работающих программных системах) верификации описаний не языке VHDL обнаружить.в литературе не удалось.

Целью работы состоит в исследовании модели CSP как средства описания проектов аппаратуры и развитие на этой основе метедов, алгоритмов и инструментальных средств доказательства корректности проектов аппаратуры.

Для достижения, поставленной цели в работе решались следующее задачи:' -

- исследование требований, налагаемых областью описания,про-

ектов аппаратных средств, обеспеченных CSP;

- исследование возможности моделирования VHDL-огщсаний на основе CSP-описаний для их дальнейшей верификации; , -

- сравнительный анализ существующих методов верификации CSP-описаний;

- разработка метода верификации CSP-описаний, рассматриваемых как проекты аппаратных средств ЭВМ;. .

- разработка алгоритма и экспериментальной программы, обеспечивающей проведение верификации проектов аппаратных средств ЭВМ.

.Методы исследования основаны на использовании понятий и Методов теории параллельных систем, вычислительных структур, формальных языков и математической логики; в работе сочетается формальный и содержательный подходы.

Научндя новизна исследования состоит в том, что:

- предложен способ верификации CSP-описаний проектов аппаратных средств ЭВМ. Отличие метода состоит в том, что за

1 счет сужения вида CSP-описаний, к которым применим метод, удалось добиться полиномиальной сложности анализа корректности взаимодействия компонентов. Метод выявляет состояния. в которых может возникать дедлок;

- предложено использование CSP' в качестве средства моделирования ряда конструкций.языка описания аппаратуры VHDL для их дальнейшей верификации.'

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

Внедрение результатов работы. Теоретические и практические результаты использовались в госбюджетных НИР кафедры ВТ в 1992-1993 гг. Полученные результаты в настоящее время подготавливаются в рамках экспериментальной системы верификации цифровых схем для использования в учебном процессе кафедры вычислительной техники ТЭТУ.

Апробация работы. Основные положение диссертационной работы докладывались и обсуждались на следующих конференциях:

- 46-й областной конференции "Актуальные проблек-j развития

радиотехники, электроники и связи" (г.Ленинград. 1991 г.);-научно-технической конференции профессорско-преподавательского состава ГЭТУ им. В.И.Ульянова (Ленина) (г.Санкт-Петербург. 1993 г.). •

Публикаций. По материалам диссертадионной работы опубликовано 2 научных статьи и i тезис доклада на конференции.

Структура и обьеи работы. Диссертационная работа.состоит из введения, четырех разделов с выводами, заключения, списка литературы, включающего 66 наименований, и 2 приложений.. Основная часть работы изложена на 139 страницах. Работа содержит 12 рисунков и 1 таблицу. -'

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

Во "введении обоснована актуальность теш, сформулирована цель и основные задачи исследования,

В первом разделе диссертационной работы рассмотрены основные аспекты языков описания проектов аппаратных средств ЭВМ. метод верификации алгоритмов Э.Дейкстры-Д.Гриса а обзор модели взаимодействующих последовательных процессов CSP. а также выполнен обзор методов верификации алгоритмов на CSP.

Суть формальной верификации, заключается в проверке соответствия между описанием реализации проекта и его функциональной спецификацией, задающей представления, о желаемом.поведении объекта проектирования. Методы верификации используют определенные правила'преобразования описания для.формирования либо заключения о правильности или неправильности проекта, либо набора условий, при которых описание реалиаадаи проекта соответствует его функциональной„спецификации. 'Заключение о правильности проекта возможно, когда соответствие между описанием и его функциональной спецификацией успешно доказывается при всех допустимых значениях входных сигналов или переменных, а заключение о. неправильйости означает, что имеются расхождения в желаемом и действительном поведениях объекта.

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

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

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

До настоящего времени проблемы верификации описаний проейтов аппаратных средств в основном были связаны с описаниями, составляемыми в рамках парадигмы последовательной алгоритмизации. Это .вызвано, в частности тем, что идея и методы верификации аппаратных средств имели источник в области теоретического программирования и программной логики Ч. Хоа-ра. Поэтому для отражения ряда особенностей аппаратуры последовательные описания, например язык охраняемых команд Э.Дейкстры, были расширены операторами, позволяющими учесть параллельное функцибнирование. Широко используемые для этой цели операторы parbegin-parendl и - cobegln-coend во-первых, отражают1 поток управления в алгоритме и это понятие не имеет смысла для аппаратных средств и, во-вторых, они имеют принципиальные ограничения. - позволяют рассматривать лишь так называемые параллельные-последовательные описания.

Что касается проблемы учета времени, то она может быть отражена в модели и методах на разных уровнях, с разной, степенью детальности. Модель CSP, как она предложена ее автором, не позволяет учитывать числовые значения временных интервалов. Однако время в этой модели отражается косвенным, но принципиальным образом - через последовательности событий.

Обзор модели CSP показывает, что CSF может обеспечить описание параллельного функционирования■компонентов в проектах аппаратных средств ЭВМ. Кроме этого, в CSP реализована модель .взаимодействующих процессов, основанная на передаче сообщений, а именно в таком режиме и работают компоненты дафровых схем. При переносе CSP в область описания проектов

аппаратных средств надо чётко установить, какие уровни абстракции и области описания обеспечены на основе CSP.

VHDL является перспективным стандартом в области языкоь аппаратуры, и поэтому верификация VHDL-опиоаний вызвала особое вйимание исследователей в этой области. Однако задача верификации VHDL-описаний оказалась довольно трудной, так как сам язык является сложным языком и формальное определение семантики VHDL отсутствует.'

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

Поэтому в соответствии с целью исследования поо-тавим следующие задачи. .

1. Исследовать возможность использования CSP как средства описания проектов аппаратных средств ЭВМ.

2. Определить семантику подмножества языка VHDL средством CSP для дальнейшей верификации VHDL-описаний.

3. Разработать метод .верификации CSP-описаний, реализация которого не должна вызвать серьезные сложности. !

. Во втором, разделе диссертационной работы выявлена область использования модели CSP при описании проектов аппаратных средств ЭВМ, определена семантика ряда конструкций языка описания аппаратуры VHDL с помощью CSP и предложен способ верификации ациклических описаний на VHDL. "'■•".

CSP может использоваться для описания проектов аппаратных средств 'на процедурном уровне 'абстракции. " Если имеется последовательный алгоритмический процесс, то он легко описывается языком CSP как один последовательный процесс с помощью арифметических и логических операторов. ; CSP поддерживает модель параллелизма на основе передачи сообщений, где не имеется понятия общей памяти.. В реальных цифровых схемах отдельные элементы работают параллельно в независимости друг от друга, пока элементу не нужно.передать ида.получить-сигналы. Такая.модель работы.легко описывается в, CSP. путем.ком-

юзиции компонентов оператором параллелизма (II). Надо заметать, что этими элементами являются или элементарные, или ¡ложные блоки. Далее описывается каждый процесс в отдельности на функциональном уровне. Если один из параллельных провесов имеет определенную структуру, то можно 'описать его уставные элементы. Другими словами, иерархическое описание фоекта аппаратных средств можно проводить с помощью СЭР. !сли структура.этого блока неизвестна, то он рассматривается сак черный ящик,• для чего определяется описание на функцио-1альном уровне. Взаимодействие- между элементами осуществляйся через каналы связи. Выходной элемент определяет значе-ше выходного сигнала. Входной элемент принимает этот сигнал го определенному каналу связи. Сигнал в канале связи не дол-ген сниматься выходным элементом, пока входной элемент не 5удет готов принять этот сигнал. В то же время, как входной элемент ждет поступление сигнала от выходного элемента и по-са он не поступил, входной элемент не может определить ни )дного из своих выходных сигналов. СБР включает синхронный гип взаимодействия. Это означает что событие взаимодействия троисходит только тогда, когда взаимодействующие процессы )ба готовы исполнить это событие. Если один из них еще не потов, то другой процесс ничего не может делать, кроме как зжидать это событие. Такое совпадение с семантикой работы щфровых. схем делает задачу описания цифровых схем легкой и толученное описание будет вполне отражать работу реальной зхемы.

Описание на непроцедурном уровне принципиально отлича-зтея от"описания на процедурном уровне. Чтобы описать проек-гы аппаратных средств на этом уровне абстракции, надо иметь возможность отражения условного выполнения действий. Язык ]БР-основан на языке охраняемых команд Дейкстры, включающем возможность представления условных команд, выполнение которых определяется охранами. Охраняемые команды Дейкстры рас-иирены в СЭР так. что охраной может быть логическое выраже-те или команда взаимодействия. В реальных цифровых схемах зыполнение определенных действий обуславливается или поступлением одного сигнала, или более чем одного сигнала, один иэ которых представляет собой синхронизирующий сигнал, или эна-

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

В данном разделе описываются базовые методы моделирова ния на YHDL и показывается, как можно составить их соответс твующие CSP-описания. Рассматривается также преобразовани предикатов для некоторых типовых конструкций VHDL. Для опи сания семантики конструкций дано представление их в виде эк вивалентных операторов на языке CSP.

Во втором разделе решается задача верификации отдельны конструкций языка VHDL с помощью CSP. Процесс верификаци может быть реализован двояко:

1) преобразование в операторы на языке CSP с сохранени ем семантики конструкций и последующая верификация получив имхся троек Хоара;

2) используемые в пункте 1 правила преобразования пре дикатов могут быть применимы для непосредственной"верифика ции конструкций языка VHDL.

В третьем разделе диссертационной работы, разработа способ верификации CSP-описаний проектов аппаратных среде! ЭВМ. Предлагаемый способ верификации можно разделить на де стадии :. последовательной верификации и верификации на уроЕ не спецификации.

На этапе последовательной верификации проверяется cooi ветствие между последовательным описанием на CSP и его пре; и постусловиями. Входными данными является описание на CSP пара утверждений. Результатом является "TRUE", "FALSE", и

условия правильности. "TRUE" означает*, что описание соответствует его пост- и предусловиям, a "FALSE" означает, что описание не соответствует этому. Условия правильности представляют собой условия на входные сигналы. При соблюдении■ этих условий алгоритм будет работать соответственно его пред- и постусловиям. Иначе работа алгоритма не будет соответствовать этим утверждениям. Для осуществления задачи верификации на данной стадии используется метод верификации алгоритмов Э.Дейкстры-Д.Гриса. Как было сказано, этот алгоритм используется для' верификации алгоритмов, написанных на языке .охраняемых команд . В CSP составляются описания последовательных процессов на основе этого языка и поэтому возможно верифицировать CSP-описания с помощью этого метода. Остается только определить предикат слабейшего предусловия для команд CSP, отсутствующих в языке охраняемых команд. Новыми командами являются команды ввода /вывода.

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

На этапе верификации, на уровне спецификации доказывает-

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

1. Проверка соответствия между протоколами Целью этой проверки является уточнение того, что последовательности событий, происходящих между составными процессами и окружением, соответствуют последовательностям., представленным в функциональной спецификации проекта, который состоит из. этих процессов. Также проверяется отсутствие дед-лока. Алгоритм, проверки назовем Уег_Рпэ1 и ему передается один из еще не проверенных протоколов спецификации. проекта. Составной процесс,' как и ранее.' будем называть элементом. Уег_Рп^ включает следующие шага ■.:

1. Сравнивается текущее (последнее) событие этого протокола с текувдми событиями из функциональных спецификаций состав-' ных элементов.-

2.- Если оно не совпадает ни с одним из. них.» то передается сообщение о несоответствии между описанным и ожидаемым поведением и работа алгоритма прекращается.

3. Если совпадение имеет место, то оба события устраняются и предыдущие события станут текущими. Протокол из спецификации составного элемента запоминается в списке протоколов.

4. Сравнивается текущее событие с. текущими событиями из протоколов. включенных в список протоколов

5. Если оно совпадает с одним из них.' то. совпадающие события устраняются, и предыдущие события .станут текущими. Если протокол из спецификации проекта станет пустым, то алгоритм успешно завершает работу, а если он еще не пустой, то управление передается на шаг (4).

6. Если оно не совпадает ни с одним из них. то сравниваются текущйе события из.протоколов составных элементов, включенных в список.

- и -

7. Если совпадает одна пара событий из них,, то они устраняются и управление передается на шаг (4).

8. Если не совпадают, то сравниваете,я текущее событие протокола из спецификации проекта с текущими событиями протоколов из спецификаций составных процессов, еще не включенных в список.

9. Если событие совпадает с одним из них, то оба устраняются и найденный протокол запоминается в списке. Затем управление передается на шаг (4).

10. Если оно не совпадает ни с одним из них, то каждое текущее событие из'протоколов, включенных в список, сравнивается с текущим событием протоколов из спецификаций составных процессов. еще не включенных в список.

11. Если' совпадает одна пара событий, то они устраняются и найденный протокол запоминается в списке. Затем управление передается на шаг (4).

. 12. Если не совпадает ни одна пара событий, то передается сообщение о появлении дедлека и алгоритм прекращает работу.

.Оценка сложности проверки соответствия между протоколами составит. - к

0((п+1). (I пи).)/ 1-»

где

п - количество событий в протоколах спецификации схемы'; 1 - количество внутренних событий среди всех протоколов

составных процессов; к - число компонентов - составных процессов; . Шд- число протоколов в 1 процессе. Правила композиции выражений используются для верификации Ёыражений функциональных спецификаций следующим образом: Для каждого выражения из функциональйой 'спецификации проекта,- определяющего отношение между одним из выходных сигналов (С) и между входными сигналами вызывается процедура ¡Мо(Ш (выражение. С). При работе она использует список выражений.

Процедура МосШ (выражение. С) включает следующие шаги : 1. Перебираются выражения из.списка для того, чтобы найти выражение., в котором сигнал. С появляется в левой части опе-

рации отношения/ в котором определяется его отношение с входными сигналами.

2. Если такое выражение не найдется, то передается сообщение о неопределенности этого сигнала и алгоритм прекращает работу. , '..-'• .

3. Если найдется такор 'выражение (С1). то вместо выражения, выбранного из спецификации проекта (С2) формируется нрвое выражение (R). 'Используется правило для формирования логического выражения левой части нового выражения, и правила для • формирования нового отношения выражения Я. !

4. Проверяются сигналы, появляющиеся в логическом выражении левой части выражения (R). Если данное логическое выражение является константой или включает только входные сигналы проекта и-сигналы из списка, то алгоритм возвращает признак успешного завершения. ;

5. Если один или более чем один сигнал не является щ входным, ни сигналом из огшока, то сначала запоминается сигнал (С) в списке, и-затем для. каждого из этихчсигналов (S) вызывается Modif (выражение,S).

Алгоритм верификации описания проекта аппаратных средств на CSP включает следующие шаги ;

Сначала верифицируются описания поставных процеосоа На CSP с их соответствующими парами пред-ц'постусловий, Это осуществляется путем использования метода верификации последовательных программ 3. Дейкстры-Д.Гриса с модификациями. Так как верификация последовательных описаний составных процессов не требует, никакой информации о поведении других процессов в системе, данный шаг можно выполнить параллельно. Это означает, что процесс верификации можно выполнить быстрее, и это является одним из положительных аспектов данного метода.

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

3. Если все CSP-описания верифицируются успешно с определением условий правильности, отличающих от 'FALSE', то на основе результатов верификации формируются функциональные спецификации для этих описаний (элементов)

4. В результате предыдущего шага, каждый элемент (процесс) в проекте будет иметь свою функциональную спецификацию. На этом шаге сначала выбирается- один И1 еще не проверенных протоколов событий из. функциональной спецификации проекта. Затем передается этот протокол в алгоритм проверки соответствия между протоколами Уег_РгоА.

5. Если алгоритм проверки неуспешно завершает .работу, то данный алгоритм прекращает работу.

6. Если алгоритм проверки соответствия успешно завершает работу, то для каждого выражения, скомпонованного с проверенным протоколом-оператором (И), вызывается алгоритм (Мо-с11П, предложенный раньше в бтадии верификации на уровне спецификации. Кроме переданного выражения, алгоритм (МойИ) имеет доступ к списку протоколов составных процессов, использованных на шаге (4) для того, чтобы использовать их в процессе верификации выражений.

7. Если алгоритм (МоаНГ) заканчивает работу неуспешно для любого из выражений спецификации проекта, то алгоритм прекращает работу, иначе минимизируются модифицированные выражения спецификации проекта.

8. Если есть•еще нёпроверенные протоколы в спецификации проекта, то управление передается в.шаг (4). Иначе алгоритм успешно прекращает работу .

В данном алгоритме протоколы и скомпонованные с ним выражения Из спецификации составных' процессов, используемые для поверки соответствия некоторого протокола из спецификации проекта, запоминаются для их дальнейшего использования при верификации выражений, скомпонованных с данный протоколом проекта. Причиной этого является то, что люоий элемент аппаратных средств может иметь разные варианты поведения. Эти варианты отражаются в спецификации этого элемента через оператор "(ИЛИ), так как в любой момент времени элемент ведет себя соответственно одному Варианту. Элемент может иметь один единственный протокол для всех вариантов функционирования или более чем один протокол. "Общим случаем является тот случай, когда для каждого варианта поведения имеется протокол событий. Задача верификации любого выражения из спецификации проекта в данном случае состоит не только в верифика-

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

В четвертом разделе диссертационной работы" представлена разработанная программа верификации и пример ее применения.

Для проведения верификации CSP-описаний проектов аппаратных средств ЭВМ разработана экспериментальная программа верификации алгоритмов по предлагаемому методу. Программа написана на языке программиррвания Турбо-Си и работает , под управлением операционной системы MS-DOS на персональных компьютерах, совместимых с IBM PC.

Входными данными для программы являются описание составных процессов проекта с помощью оператора параллелизма,-функциональная спецификация каждого составного процесса либо его поведенческое описание на CSP с парой пред- и постусловий и функциональная спецификация проекта. Функциональная спецификация и пред- и постусловия формулируются на языке логики предикатов без использования кванторов: Дт составлен, ния поведенческих.описаний составных процессов используются все команды языка CSP, используемые для составления последовательных процессов, кроме команды цикла и включая команды ввода/вывода. Программа зафиксирует ситуации, где может возникнуть дедлок при работе проекта. Кроме этого, она проверяет .соответствие между реализацией составного процесса (то есть его поведенческим описанием) и его функциональной"" спецификацией. а также соответствие между реализацией проекта (то есть его параллельным описанием) . и его функциональной спецификацией." Дедлок отражает тот случай в выборе цифровых схем, когда выходной сигнал.любого элемента передается перед тем, как определяются все'его входные сигналы. Также программа верификации может определять условия на значения входных сигналов, при соблюдении которых процесс будет функционировать соответственно заданному постусловию.

Приведен пример верификации части проекта аппаратных

средств ЭВМ с-помощью Предложенного в диссертационной работе метода верификаций CSP-описаний. Фрагменты протокола верификации приведены в приложении 2.

В приложении 1 приводятся примеры- верификации CSP-описаний с помощью известных методов верификации. CSP-алгорит-мов. предложенных в первом разделе.

В приложении 2 приведен .протокол верификации для примера из п. 412

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

В результате проведенного ' исследования были получены следующие результаты.

1. Выявлена область использования модели CSP при описании проектов аппаратных средств: CSP подходит для описания на регистровом и более высоких уровнях, на которых выполняется логическое проектирование аппаратуры без учета значений временных интервалов.. Также отмечено, что CSP обеспечивает составление структурного описания и поведенческого описания.

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

3. Предложен способ верификации ряда конструкций языка описания аппаратуры VHDL, отличающийся использованием языка CSP и обеспечивающий применение метода верификации Э.Дейк-стры - Д.Гриса к VHDL-qjracaHHflM аппаратных средств. Возможна реализаций способа в одном из двух вариантов: либо преобразование VHDL-конструкций в CSP-описания с последующей верификацией. . либо использование полученных преобразователей предикатов непосредственно для VHDL-описаний.

4. Предложен метод верификации CSP-описаний проектов аппаратных средств ЭВМ. Отличие метода состоит в том, что за счет сужения вида CSP-описаний, к которым применим метод (описание с протоколами конечной длины либо бесконечными периодическими протоколами и без использования команды цикла

при составлении"поведенческих описаний)., удалось добиться полиномиальной сложности анализа корректности взаимодействия компонентов. "Метод выявляет состояния, в которых может возникать дедлок. разработан алгоритм, реализующий процедуру верификации с,применением данного метода,

5,. Разработана программана основе предлагаемого метода для верификации проектов ещпаратных средств, составленных на СБР, Входное описание.может отражать параллельность функционирования компонентов проекта- и обратные связи.

••■ ПУБЛИКАЦИИ. ПО ТЕМЕ ДИССЕРТАЦИИ

1. Али А.Мохаммад., Распределение вычисления на древообразных стрз(ктурах // Актуальные проблемы развития радиотехники, электроники и связи: Тез. докл.' 46-й областной йаучно-техничбской ■•конференции.- Л.-1991.--' С. 54-55.

2. Горянкин А. В.. Али А. Мохаммад. Параллельные'^описания цифровых схем для их верификации //; Изв. ЭТИ: Сб. науч. тр./ Санкт-Петербургский ■ электротехн. ин-т им. В, И. Ульянова (Ленина). - . Санкт-Петербург.- 1992,-Вып.444.- С.46-48......

3. Али А. Мохаммад, Хохловский В. И. Щ использовании СБР как языка описания цифровых устройств // Изв. ,;ГЭТУ: Сб. науч. тр./ СПБ. государ, электротехн. университет им. В. И. Ульянова (Ленина).- Санкт-Петербург,-1993.- ВЫП. 458.- С.46-48.

Подписано в печать 01.06.94. формат 60x84 1/16.

Офсетная печать. Печ.л. 1,0; уч.-из^. л. 1,0.

Тираж 100 экз. Зак.Ца

Ротапринт МГП "Поликом" 197376, Санкт-Петербург, ул. Проф. Попова. 5