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

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

ГОРЯНКИН Андрей Владимирович

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

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

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

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

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

Оаккт-Яетарс^рг -

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

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

доктор технических наук профессор ПЛОТНИКОВ A.B. Официальные оппонента:

доктор технических неук профессор НЕЫОЛОЧНОВ 0.05. кандидат технических ввук доцент ТАТ1РШЮВ D.O.

Ведущая организация - ЛКТБ ЛОЭП "Светлана"

Защита диссертации состоится * ^ " HS'^offi 1992 1 в 1° часов на заседании специализированного сове: К 063.36.12 Оанкт-ПетерСургсвого ордена Ленина и орде! Октябрьской Ревашищи электротехнического института тег В.И.Ульянова (Ленина) по адресу: 197376, Санхт-Пзтербурз ул.Проф.Попова, 5.

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

Л ^

Автореферат разослан е^ТЯ <>/# 1992 г.

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

Балакин ЬЛ

- 1 -

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

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

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

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

-г -

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

агП

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

Другая проблема, несколько менее известная, состоит в том, что задаче формальной верификаций, являясь элементом задачи анализа, в этом смысле дуальна задаче синтеза, как известно, в общем случае алгоритмически-неразрешимой. Следовательно, есть основания ожидать и неразрешимости общей постановки задачи ве-рификацяв. Имеются работы, в которых утверкдается, что госта-аоака задача полной верЕфвкадзг '¿йр&?$шт) практически б-эс-сшслепна, тек как единственный способ доказательства правильности в данном случае - восстановить цостроение программы.

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

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

- з -

остроту проблем и, зачастую, конкретное решение выводит задачу из класса НР-полннх.

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

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

Для достикания поставленной цели з работе решались следуйте задачи:

- сравнительный анализ суцесгвумцих методов веркфикащш проектов аппаратных средств ЗВМ;

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

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

- исследование возможных способов учета временных характеристик компонентов проектов аппаратных средств ЗВМ, повышащих степень адекватности разработанных методов верификации;

- анализ трудностей, возникащих при верификации списаний :;рзектов аппаратных средств ЗВУ с учетом времени и, на бгой остове, разработка способа интерпретации результатов взрифаквции з учетом времени в виде временных диаграмм;

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

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

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

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

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

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

Практическую ценность работы представляют:

- разработанный способ упрощения интерпретации результатов верификации описаний проектов аппаратных средств ЗШ с учете« времени, основанный на автоматическом построении определяем результатом.временных диаграмм;

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

Внедрение результатов работа. Основные результаты работе использованы в двух научно-исследовательских работах, выполненных на кафедре вычислительной техники Свнкт-Петербургскоп влвктротехотческого института:

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

- хоздоговорной научно-исследовательской работе, связанно.

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

Результата работы также внедрены в учебный процесс на кафедре вычислительной техники названного института к в тачепш трех лет используптся при проведении лабораторных работ а райках курса "Метода проектирования и САПР ЭВМ".

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

- республиканской научной конференции молодых учеши п специалистов г. Чебоксары (г.Чебоксарп, 1950г.);

- 46-Л областной паучш-теащчеекс;! конференции "Актуальные проблет развития радиотехники, электроники и связи" (г.Лепипг-рад, 13Э1г.);

- еззгодашх цагдга-техшчзаккх конференций: профессорско-пргшдев-тельского состава алеагротехвдчесясого аастктутз г.Лй-нинграда (г .Ленинград, 1950-1552гг.).

Цублнкацав. По материалам дассаргоциовюЗ: работы ощбя&'о-ейно 3 печатных работа. К моменту нвшгсанил диссертации з печати находятся еще Б работ.

Структура и обьаи работы, Дкса&ртацаошая работа состоит из введения, четырех разделов с кшздаиа, заклшс-яия, списка литературы, ЕКПШ8!аД5ГО 1С9 ншйэновшзй!, В лпгллоненля. Основная часть работы изложена на П7 страницах ГАапшописного текста. Работа содержит 23 рисунка и 5 твблщ.

ОСНОВНОЕ СОДЕКШШ РАБОТЫ

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

В первогл разделе диссертационной работа выполнен обзор методов верификации ахшаратшг средств ЭВМ.

Развитие методов формальной вэрификвции проектов аппаратшя: срздсгз ЭВМ продиктовано потребностью проверки правильности проектов бллшой сложности. Суть фор?лальной верификации заклю-чьэгся в проверке соответствия и&аду описанием реализации проекта ¿1 его функциональной спецификацией, задачей представления о желаемом ловед>:н;:л объекта проектирования.

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

Следовательно, задача верификации проектов аппаратных средств ЭШ состоит в определении условий, при которых описание реализации проекта аппаратуры ЭВМ соответствует его функциональной спецификации.

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

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

Кетода верифякаирш программных средств ЭВМ не могут передеть перечисленные особенности функционирования компонентов аппаратных средств ЭВМ, поэтому возникает необходимость разрабв-

тывать специализированные метода» ориентированные непосредственно на область верификации ашгарзтурц. Обзор наиболее перспективных методов верификации аппаратных средств ЭВМ составляет основу первого раздела диссертационной работы.

В разделе выполнен анализ основных из существущих методов верификации аппаратных средств ЗВЫ, включающий такие группы методов , как: маюда, построенные на основе темпоральных и интервальных логик; методы, использушцке автоматные и графовые модели; алгебраические метода; метода верификации параллельных программ. По результатам анализа проведено качественное сравнение рассмотренных, методов верификации, позволявшее сделать вывод, что одним из перспективных методов верификации является метод верификации последовательных алгоритмов Э.Дейкстры, допускающий обобщение на случай верификации параллельных алгоритмов..

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

При переносе метода верификации Э.Дейкстры в новую для него предметную область верификации описаний проектов аппаратуры ЭВМ ваашш является учет временных характеристик -компонентов проектов - свойства отсутствующего в исходной постановке задачи данного метода. Учет временных характеристик компонентов существенно влияет на точность проведения верификации проектов аппаратных средств ЗВЫ.

В соответствии с целью исследования поставлена задача:

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

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

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

- в -

оператора определения параллельного сегменте (раг-оператора), где <StJ> обозначает произвольный опервтор некоторого языка программирования, такой, что его выполнение в параллельной вычислительной системе неделимо.

b^1,...Ью1:«true,...true;

Ь„„,...Ъ :-Га1вэ,...Га1ве;

12 RSI

bn,b12:=f alee, true

parbegtn

<S„>; ... <S1)9>

// <S„,>; ... <s >

ml run

parent!

B)

dob,, -> S„

» ья; :> smt

" ~> Smr,

trsn шп

od Рис. 1

bie:«=íalae

b„, ,b „:<falae,true

Ш1 Ш2

Ъ'.-false

ВфЪ

б)

Предлагаешй в диссертационной работе подход основан на сведении верификации параллельных описаний рис. 1,а к верификации их циклических последовательных недетерминированных моделей вида рис. 1,6. Для верификации моделей использована семантика слабейшего предусловия (яр-семантика) З.Дейкстры, принцип нз-шдншгной точки в интерпретации АЛагаЫ. и основанный на принципе метод верификации циклов, рассматриваемый Е.С.Н.Не1шег.

Оператор языка охраняемых команд З.Дейкстры "<1о Ь -> 3 ой" семантически эквивалентен следующей рекурсивной функции Ш « II Ь -> 3; КЗ С ] Б -> аИр 11 { Н },

оледовптельно, результаты верификации втих двух конструкций относительно одинакового постусловия И совпадают: яр(ба, Н) -чф(Ш, Я). 11оото?лу слабейшее предусловие оператора цикла равно

*р(йо, И) * (Ь яр (Б, 5ф(Ш, Е))аг(Б « ир(ак1р, К)), вяа после упрощений я переобозначения Х»*р(йо,Н):

I - Ъ&яр(Б, X) у 5&В. (1)

Уравнения вида (1) являются одной из составных частей предлагаемых в данном разделе диссертационной рвботы методов верп-

фикации. В литература доказаны существование решения (1), единственность решения, способ вычисления и покапано, что vtp/wlp-семантики, при выполнении свойств й/ИЯИ-непрер^ости, соответствуют следущим общим решениям:

яр (do, R) = (an: пей: wpn(ialae)), wlp(do, R) = (Vn: n « H; tflpn(true)).

На основе ^шенетгая рассмотренного подхода к верификация циклической модели рис. 1 ,б в диссертационной работе» по индукции, было получено выражение, сводящее верификнцгао раг-шеззвто-ра рис. 1,в s верификации перестановок его соствншк нэптз!: яр (par, Н) = (VI: « Ю): ЩЩ^, (2)

где D - множество номеров перестановок, зе вврдгаЕгщз: порядок следования Sk в ветвях искадеогэ рагмтертгер». В ®г®гтве Sk здесь выступают операторы ззгаей, индекса шщзые перенумерованы, а величина п. содасгаавезз свя&щ шшцг тваих операторов;

П^ - обозначает 1-я яерестгдазку из я опврвторзэ Зк, объединяющих оператора S.Ja отдааезх еетвей par.

Сложность шчисяеааа (2J Езйюзанциальноя а хвраяяврщувтся количеством необходимое дяя пкпшшешш верифтецга Енрггзтов перестановок операгорсз Эта азяасчгна равна:

Н = п!/(ш,}.аа!....ар«>, (3)

где п^ - коятгестзо саерзторсгв 1-й аагви par;

п - колзчэвтво утасязтязвх в перестановках операторов; р - КОЛИвОГВО В2ТЕ2Й рзг-одвраторз. Для сшвеняя отгости sepгфшшда параллельных описаний по (2) во втором разды® рассматривается способ уменьшения количества вявлязаруейах сзрэстзяхят, осшзванннй на побятии нзвза-и,гаде®ствня опарзторсз опгсанал. йэвзаишдействувдши считается такие оператора ле6с£ сяоаностя, что на одаа из операторов присваивания одного из них не изменяет пропзвэльнуо перзнашуа другого. Оператора июда таете счзшштся ооераторгг-са прнсваявз-

ЕШЯ.

Известно, что порадоя вдагогаого вшюлнаши группа параллельных невзвимодейвтзупцях го данным и управлении операторов зе влияет на результат вычисления. Применительно s верификацзз это означает всзмоаность прл построении (2) пропускать rapocis-

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

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

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

Сложность предлагаемого способа уменьшения перебора при верификации полиномиальная - 0(п3), следовательно способ является аффективным. Выигрыш от применения способа определяется свойствами конкретного раг-оператора. В худаем случае, при полном взаимодействии операторов, выигрыш отсутствует, а в лучшем случае, при полном невзаимодействии, составляет величину на единицу меньшую задаваемой выражением (3).

В разделе рассматривается возможность использования операторов синхронизации параллельных процессов "await Exp then S" при верификации и предлагаются правила построения соответствующих графов отношений.

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

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

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

По определению А-програкма есть совокупность пар вида:

Ъ, -> V • - • Ьп -> V

где bt - условие запуске; Sj^ - оператор, выполняющийся при истинном Ь^.

А-программа работает в дискретном времени. ее оператора взаимодействуют над общей памятью, а интерпретация А-прогрвммн такова, что при истинности произвольного количества условий ЬА запускаются некоторые (возможно вез) пары, операторы которых выполнился параллельно. IIa структуру операторов ограничений ks накладывается, следовательно возможна их иерархическая организация.

Бо втором разделе диссертационной работа показана возможность применения А-прогрвмм для описания поведений 'Ьроекткруе-них аппаратных ергдетв ЭВМ. Такие описания зазваны асинхронными (А-описания).

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

Верификация предложенных моделей А-описапия, з принциде.

сводится к методу рассмотренному вша для моделей параллельного описания. Анализ особенностей, функционирования аппаратных средств ЭВМ показывает, однако, наличие ситуаций, когда верификация ¿-описаний в терминах т?р/и1р-семанткк оказывается невоз-цохнок. Это связано с особенностью понятия заверит,«оста: процессов в цифровых устройствах. Имеются случаи, когда процессы в устройствах незснераиш и, следовательно, верификация е терминах яр-семантики навозмонна. Использование «Хр-семаитика: таете представляется навозкоаным, из-за показанных в разделе недостатков етой семантики.

Для верифгквциз возможно Ееаавзршп?,их цтпютгесяих моделей А-оиисаннй в диссертационной работа предлагав гдгтод вернфакадан основанный на ир-егмаптнке г принципе негодвягной точки. В ре-боте выполнено теоретическое оЯоозованпз кгтодя, приводятся ггрхзлзрн вернХпк&цги. Варгфкацгта моделей ссадепя к птергтяйнтгу резаюха уравнения вида (1), для начального приближения равного лраЕарйаыовд а цикла условии Я. Обп;ае решгпгс ургвнэпяя (1):

гПр(с1о, Н) --- (зп: п. с К: яр (Е))» где й!р - обозначение для зведэнной во вторег-л разделе дкссерга-щюшой работы семантики слабсйпаго инвариантного предусловия.

В разделе показано, что для вввершких циклов и!р(йо, И) = «р(йо, К), а в случив казавериЕг^зго цакла Лр-сомантика опредз-ляет его инвариант, причем болеа сильный чем задаваемый тг1р-со-ыантикой: к1р(<Ю, К) ^ с1р(1о, Н).

¿налогов предложенного во втором раздела диссертационной работы метода верификации еозшнео незвверяшмых ¿-описаний в литературе не найдено.

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

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

нагрузки в среде, верификация проектов аппаратуры ЭВМ предъявляет более строгие требования к учету времени. При верификации аппаратуры относительные понятия обычно заменяются на абсолютные значения времени, например, раньше на 10 не, позке но 2 такта и так далее. Кроме того, появляется такие понятия как помехи во вход»-г сигналах, нестабильность выходных сигналов, время распространения сигнале от входа к выходу и прочие. Все вто разнообразие понятий существенно для определения правильности функционирования цифрового устройства.

Из набора представленных, во введении к денному разделу способов учета времени для целей-верификации параллельных описаний проектов аппаратуры ЭВМ представляют интерес: способ, учитываэ-щий время и качестве параметра описания; способ, использующий (функции от времени; способ, основанный на функциональных моделях компонентов проекта,- предложенных А.О.Тишзфеевнм. Зти три способа исследуются с целью определения возможности та использования при веркфшеацки описаний проектов аппаратуры ЭЕМ.

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

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

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

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

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

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

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

Для проведения верификации циклических процедурных и параллельных описаний проектов аппаратных средств ЭВМ разработана экспериментальная программа верификации алгоритмов по методу 3 ..Дейк с три. Программа написана на языке программирования Турбо-Паскзль и работает под управлением операционной системы КБ DOS версии 5.0 на персональных компьютерах, совместимых с IBK PC. Объем исходного текста программы 7000 строк.

Вхбдшми данными для программы являются функциональная спецификация, записанная в виде предусловия и постусловия (предикатов без кванторов), к циклическое процедурное или параллельное описание реализации проекта ашшратуры ЭВМ, представленное на языке, близком к языку охрпняемых комазд Э.Дейкстры. Результатом ряй-лк программ* якяяетея предикат, определяющий условие правильности функционирования проекта ашшратуры ЭВМ.

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

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

ОСНОВНЫЕ ЕЕЗУЛИШа 1ШЮТЫ

В ходе проведенного исоледованга бйии подучены слеодтацжз основные результаты.

1. Предложен формально обссззвянЕнй метод вери^кжхта параллельных описаний проектов еезэраишх среди® ЗЕЗ&. Рааработв-нн эффективный способ уманяаешиг вытаслятельной" елггавпета катода, основанный на прижила квзатшодействувдих операторов списания, е алгоритм, резлжщарй процедуру зери$иквцяи с применением способа. Простота вягоритма делает удобным его использование в автоматизированиях системах- вергфйкппш, что является основным отлютем прэдлоаеткта метода от изыгстннх.

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

3. Выполнен шшлиа слояности метода верификации поске.говя-гельшх алгоритмов Э.Дейкстря, полокепяого в основу прадяояен-!шх методов вери^икзшгм явраллвлыпгг и асикхрс.яннх отксянкй троектов аппаратных средств ЭеМ. Получены оценки раота размеров

предикатов при выполнении варвфаквциа по методу Э.Дейкстры. Анализ ажшшсги данного метода в литературе не обнаружен.

4..Цредлоиен способ упрощения интерпретации результатов вэ-рфквщш параллельных и асинхронных описаний аппаратных орадогв ЗШ с учетом времени. Способ позволяет предотавить результат веркХакации описания о учетом времени в удобной для проектировщика форме - в виде набора временных диаграш. Способ формализован, доведен до уровня алгоритма реализации. Предложены отвечащве способу правила составления функциональных спецификаций описаний проектов аппаратных средств ЭШ а учетом врв-шни.

5. Разработана программа для верификации циклических процедурных описаний проектов аппаратных средств БИЛ, допускавдая использование параллельных операторов непосредственно в описавши и асинхронных операторов - через циклические недетершши-ровашае модели, которые ыошэ организовывать в макроопределения. Праграша позволяет создавать библиотеки макроопределений к имеет развитые средства управления процессам верификации. Дет удобства работы пользователей создано описание применения программы.

шшшда по тш диссертации

1. Горянкин A.B. Верификация проектов цифровых . устройств // Научная конференция молодых ученых и специалистов г.Чебоксары: Тезисы докладов.- Чуваш, ун-т.- Чебоксары,"1990.-0.145. '

2. Горянкин A.B. Синтез схем цифровых устройств по верифицированным описаниям // Проектирование гаециашгаированшя средств автоматики и вычислительной техники: Межвуз. сб науч. тр. / Чуваш.- ун-т.- Чебоксары, 1990.- С.29-34.

3. Горянкин A.B. . Способ верификации параллельных описани проектов цифровых устройств с учетом времени // Областня научно-техническая конференция "Актуальные проблею разви тия радиотехники, влектроники и связи": Тезисы докладов. Д.,19910.48.