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

2 7 МАЙ Ю97

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

Харитонов Михаил Юрьевич

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

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

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

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

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

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

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

кандидат технических наук, доцент Хохловский В.Н Официальные оппоненты:

доктор технических наук, профессор Сольницев р.И. кандидат технических наук, доцент Губкин А.Ф.

Ведущая организация - НПО "Импульс"

Защита состоится "_"__ 1997 г. в_часов

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

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

Автореферат разослан "_" _1997 г.

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

Маркин А.С.

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

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

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

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

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

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

-2в

матического сопроцессора транспьютера Inmos TMS T80Ö.

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

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

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

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

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

- исследование причин, осложняющих процесс верификации, и разработка алгоритма распараллеливания процесса верификации на основе анализа спецификации проекта;

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

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

-разработка алгоритмов и экспериментальной программной системы,

обеспечивающей выполнение параллельной верификации проектов аппаратных средств вычислительной техники.

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

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

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

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

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

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

-обзор существующих методов верификации проектов аппаратных средств ЭВМ;

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

Внедрение результатов работы. Основные теоретические и практические результаты работы использовались в госбюджетных научно-исследовательских работах, выполненных на кафедре вычислительной техники Санкт-Петербургского государственного электротехнического университета в 1994-1995гг. Разработанная программная система верификации используется в учебном процессе на кафедрах вычислительной техники СПб ГЭТУ и Чувашского государственного университета (г.Чебоксары).

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

- Международная научно-техническая конференция «Диагностика, информатика и метрология - 94» (г. Санкт-Петербург, 1994г.);'

-50-й и 51-й областные научно-технические конференции СПб НТО ЮС имени А.С.Попова (г. Санкт-Петербург, 1995-1996гг.).

Публикации. По материалам диссертационной работы опубликовано 5 печатных работ, из них 1 статья и 4 тезисов докладов на конференциях.

Структура и объем работы. Диссертационная работа состоит из введения, четырех разделов с выводами, заключения, списка литературы, включающего 97 наименований, и 3 приложений. Основная часть работы изложена на 109 страницах машинописного текста. Работа содержит 28 рисунков и 7 таблиц. .

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

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

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

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

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

В обзоре выделены и рассмотрены три крупные группы методов верификации:

-методы;'основанные на применении темпоральной логики и языков описания конечных автоматов;

-методы, основанные на логиках предикатов первого и высших порядков;

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

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

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

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

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

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

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

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

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

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

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

Выполненный в диссертационной работе сравнительный анализ показал, что выбранным критериям наиболее Полно соответствует группа методов, основанных на аксиоматическом подходе Хоара и w/7-семантике Дейкст-ры: эти методы при удовлетворительной трудности проведения верификации обладают высокими выразительными возможностями.

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

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

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

Предложенный в работе параллельный алгоритм верификации опирается на формальное представление схемы верифицируемого устройства ориентированным графом 0(У,0), где V - множество вершин графа, О - множество дуг. Каждому функциональному элементу схемы ставится в соответствие вершина графа; дуги графа соответствуют связям между элементами. Вырабатываемые сигналы образуют множество сигналов Б (в котором выделяется подмножество У выходных сигналов), а входные сигналы схемы образуют множество входных сигналов X. Каждая вершина графа помечается именем формируемого соответствующим элементом схемы сигнала л из множества 8, и функцией /„ описывающей зависимость сигнала 5 от входных сигналов элемента схемы. Для каждого входного сигнала л„ л,еХ, в Г|. • годятся вершины с меткой .V, и функцией /()=хг

В работе предложен следующий параллельный алгоритм верификации. ГЦ. Используя помечающие функции обрабатываемых вершин, получить выражения, связывающие входные и выходные сигналы этих вершин: V/: / = 1,|>1: получить у, =/,.(/„..,/„) П2. Для каждого из полученных на предыдущем шаге выражений: Если в правой части выражения присутствуют только входные сигналы V,, .у,еХ, схемы:

то для данного выражения дальнейшие преобразования не требуются; осуществит^ переход (для процесса обработки данного выражения) к Д4 алгоритма.

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

(V/,,(/„..,/j: '=4*1; v/y h 6: получить /, = /,/*,„■.*„)

ПЗ. Подставить полученные на предыдущем шаге выражения для внутренних сигналов в выражения, полученные в Ш. (в случае первой итерации) или при предыдущем выполнении Щ (в случае последующих итераций).

V/,:J6[1,4 IjBS-.l^f^-K)

Перейти к П2.

П4. Полученные в результате работы алгоритма выражения у,- = /у.(х) описывают действительно формируемые схемой выходные сигналы, в то время как в спецификации заданы требуемые заколы у,- = f* (х) формирования выходных сигналов. Чтобы установить соответствие описания и спецификации, выполнить операцию импликации: /у. (х)=> f*.(x). ■

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

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

имеется команда Б оплсання и предикат Я постусловия этой команды. Для преобразователя предикатов пр выполняются следующие свойства.

Дистрибутивность конъюнкции: если Я = /?,& й2&...&/?,. то *р(5, /?,)&...&нр(5, /?,) = Я1&Р.2&....&РГ).

Если известно, что выполнение команды Б детерминировано, то: /?,)Vи/,(5,Яг) = Л,

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

1) Инициализация:

a) прочитать задание на верификацию, состоящее из описания проекта и спецификации;

b) выделить в спецификации предикат постусловия;

c) инициализировать счетчик сформированных задач: ТазкСоиг^ег: -0;

2) Формирование задач:

a) пока ТазкСош^ег<= (МАХТАБК-Х)

если можно отдеяигь от постусловия конъюнктивный или дизъюнктивный член, то •

- отделить;

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

- подставить в постусловие вместо отделенного фрагмента вспомогательную переменную ТАЭКпп, где пп - равно значению переменной ТазкСоиг^ег;

- увеличить значение счетчика: ТаэкСоипйег :=ТазкСоипЬег И; конец_если;

b) конец_пока;

c) создать задачу, состоящую из описания и спецификации, в которой полное постусловие заменено на оставшуюся, неотделяемую часть:

(1) подставить в постусловие вместо неотделяемого фрагмента вспомогательную переменную ТАЭКгт, где пп - равно значению переменной ТаэкСоипЪег;

е) увеличить значение счетчика: ТазкСоипЬег: =ТазкСонпг.ег ? !: .

3) Вычисление слабейших предуслових для всех сформированных залач:

4) Объединение результатов:

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

b) Для каждой из решенных на шаге 3) алгоритма задач в предикат постусловия вместо вспомогательной переменной ТАБКпп, где пп - номер задачи, подставить предикат слабейшего предусловия, полученный'в результате решения данной задачи. *

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

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

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

^Доказательство корректности описания реализации по отношению к функциональной спецификации.

2) Доказательство выполнения в проектируемом устройстве соотношений. заданных ВД. Такое доказательство предлагается проводить следующим образом.

a) Представление описания реализации проекта в виде графа схемы в соответствии с временными свойствами структурных компонентов проекта.

b) Представление ВД в виде сигнального графа.

Графы, получаемые на этапах а) и Ь), являются ориентированными и имеют разметку как дуг, так и вершин, с) Доказательство соответствия сигнального графа и графа схемы.

В 'диссертационной работе рассматриваются идеализированные ВД, отражающие логические изменения сигналов во времени. На ВД рассматриваются четыре типа изменений сигналов, образующих множество С=(+1, -1, СН, БТ}, где первые три элемента обозначают: фронт сигнала, спад сигнала, произвольное изменение (нас интересует лишь сам факт изменения, а не какое конкретно изменение произошло). ВД может задавать также требования к сохранению сигналом своего значения в течение некоторого определенного интервала времени. Для отражения этого требования служит четвертый элемент множества. Сигналы, вырабатываемые устройством, и подаваемые'на него извне, образуют множество сигналов Б. Изменение сигнала з, зеБ, будем обозначать с(в), с^еС. ВД может задавать либо минимально, либо максимально допустимые интервалы между изменениями сигналов; вид этих интервалов может указываться явно или подразумеваться, однако в каждом случае он считается определенным. Для отражения временных свойств объекта вводится множество значений временных задержек Т.

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

1) /у Каждая вершина V,е V, помечена именем сигналам, ¿еБ.

2) Каждая вершина К,, К,е V, помечена изменением с(.ч) сигнала .у.

3) /г:£>—»Т Каждая дуга с1, ЛО, взвешена значением из множества временных задержек Т.

Граф строится для заданного описания следующим образом. Каждому множеству эквипотенциальных точек схемы с именем сигнала ^ ставится в соответствие вершина V,- графа. Имя сигнала .у становится меткой вершины Уг Изменения сигналов с(в) присваиваются в соответствии с ВД входным сигналам устройства и запоминаются заданные ВД начальные значения "неизменяющихся" сигналов. Определяются изменения остальных сигналов устройства. Далее определяется, сохраняются ли начальные значения "неизменяющихся" сигналов? Если эти значения сохраняются, то таким вершинам приписывается изменение с(з)-5Т. В противном случае можно зафиксировать наличие ошибки в проекте уже на этапе построения графа, до верификации временных свойств. Две вершины Vi и У} соединяются дугой • с!(У^Ур в том случае, если сигнал/5(У}) формируется компонентом устройства, входным сигналом которого является сигнал/х(Г^. Дуга {УьУ} взве-

шивается значением временной задержкираспространения сигнала в данном компоненте.

Формальным представлением ВД служит сигнальный граф - ориентированный граф Со(\У,Е), где - множество верши, Е - множество дуг. Граф Оо(>У,Е) имеет три функции разметки.

1) к5: Я Каждая вершина помечена именем сигнала .геБ.

2)Ас:Ж-»С Каждая вершина Щ, ЩеШ, помечена изменением с(з) сигнала 5.

3)ИТ:Е-*Г Каждая дуга е, ееЕ, взвешена значением из множества временных задержек Т.

Каждому изменению сигнала на ВД ставится в соответствие вершина Щ, которая помечается именем сигнала з и его изменением с(з). Две вершины Щ и Щ соединяются дугой е ( Щ, Щ ) в том случае, если ВД задает временной интервал между событиями, представляемыми вершинами Щ и Щ. Если событие, представляемое вершиной Щ, произошло в момент времени ¡¡, а событие, представляемое вершиной Щ, произошло в момент времени ¡¡, то дуга е{ Щ, Щ) взвешивается значением (1,-1у).

Задача доказательства выполнения в проекте временных соотношений, заданных спецификацией, формулируется в работе следующим образом: граф ВД Со(\^,Е) должен быть изоморфным подграфу транзитивного замыкания 01(У,01) графа схемы С(У,0). Помимо обычных графо-теоретических требований к изоморфности, должно присутствовать соответствие между разметками вершин и между весами дуг. Будем считать, что изменение с, сигнала соответствует изменению с2, если оба этих изменения принадлежат к одному и тому же типу "+1", "-1" или "БТ", или одно из этих изменений является изменением типа "СН", а другое не принадлежит типу "БТ":

(с,=+1 & с,=+1) V (с,=-1 & с,=-1) V (с,=БТ & сг=БТ) V V (с,=СН & с^БТ) V (с^БТ & сг=СН)

Следует также заметить, что ВД может задавать как минимально, так и максимально допустимые интервалы между изменениями сигналов. В том случае, когда ВД задает минимально допустимые интервалы, временная задержка дуги 0^,0,) должна быть не меньше временной задержки соответствующей дуги Со^,Е). Если ВД задает максимально допустимые интервалы, то временная задержка дуги 0^,00 должна быть не больше временной задержки соответствующей дуги Со^.Е).

Пусть \У| и \У> - вершины графа Со(^У,Е), соединенные дугой е <\У),У/2). Пусть также V) и V: - соответствующие вершины графа С|(У,01), которые явились результатом поиска изоморфизма непомеченных графов во и ви

Пусть эти вершины У| и соединены дугой 4 <У|,Уг). В таком случае упоминавшееся выше соответствие разметок и весов означает.

Совпадение имен сигналов соответствующих вершин графов и Оо.

2) ) = ) V Гс(У^СН8сИс(Щ) * 5ГV/с(1\) * = СИ

/сО^)=М";)^/с{уг) = БТV/С(К2) *8Т&ИС(Ж2) = С//

Непротиворечивость изменений сигналов соответствующих вершин графов С| и Оо.

3) /г^Л^Ч^у^)) или

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

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

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

1.Представить спецификацию верифицируемого проекта в виде совокупности двух частей: функциональная часть и процедурная часть.

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

3.Произвести доказательство выполнения в проектируемом устройстве заданных временной диаграммой соотношений предложенным методом:

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

- представить заданную временную диаграмму в виде графа;

- найти граф транзитивного замыкания графа схемы;

- найти в графе транзитивного замыкания графа схемы подграф, изоморфный графу временной диа!раммы.

Объединить полученные на этапах 2 и 3 результаты и сформулировать заключение о правильности проекта в целом.Ш

Для осуществления программной поддержки выполнения процедуры верификации проектов аппаратных средств разработана экспериментальная ' программная система (ПС) верификации. ПС обеспечивает проведение параллельной верификации на основе анализа постусловия спецификации проекта. Программа написана на языке программирования Си и работает под управлением операционной системы MS-DOS на персональных компьютерах, совместимых с IBM PC. _

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

Параллельность работы компонентов программной системы моделировалась при помощи нескольких персональных компьютеров соединенных в локальную сеть. В целях сравнения те же примеры верифицировались при помощи разработанной ранее на кафедре вычислительной техники СПб ГЭТУ последовательной (не использующей распараллеливание) системы верификации. Рассмотрены примеры верификации проектов цифровых устройств при помощи разработанной программной системы и проанализированы полученные экспериментальные результаты. Применение разработанной системы позволило добиться на исследованных примерах сокращения Времени верификации в 2-8 раз по сравнению с последовательной системой.

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

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

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

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

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

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

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

4. Предложена инженерная методика выполнения процедуры верификации проектов аппаратных средств ВТ, основанная на применении разработанного метода и алгоритмов.

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

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

1. Хохловский В.Н., Харитонов М.Ю. Возможности методов формальной верификации цифровых схем при построении тестов. // Тезисы докладов научно-технической конференции "Диагностика, информатика и метрология - 94", 28-30 июня 1994г. - СПб, СПб ЭТУ, СПб отделение информатики Международной Академии Информатизации. - Кн. 1, с. 132-133.

2. Харитонов М.Ю. Верификация цифровых схем в вычислительной системе с транспьютерной матрицей. // Тезисы докладов 50-й научно-технической конференции СПб НТО РЭС им. А.С.Попова, апрель 1995г.-СПб, 1995-C.41.

I 3. Харитонов М.Ю. Об опыте эксплуатации экспериментальной программной системы верификации цифровых схем в вычислительной системе с массовым параллелизмом. // "Анализ и синтез специализированных средств автоматики и вычислительной техники" : Сб. научных трудов. - Чебоксары, 1995. - с.62-64.

4. Харитонов М.Ю., Хохловский В.Н. Проблемы учета времени при верификации цифровых схем. // Тезисы докладов 51-й научно-технической конференции СПб НТО РЭС им. А.С.Попова, апрель 1996г.- СПб, 1996.-с.70-71.

5. Харитонов М.Ю., Чугунов Г.В. Эффективные процедуры обработки булевых функций. //Тезисы докладов 51-й научно-технической конференции СПб НТО РЭС им. А.С.Попова, апрель 1996г.- СПб, 1996.- с.71.