Введение к работе
Актуальность проблемы. Интенсивное развитие средств вычислительной техники, и расширение областей ее применения тесно связаны с совершенствованием методов проектирования аппаратных средств. Известно, что прежде чем реализовать проект аппаратных средств, надо продемонстрировать, что этот проект будет удовлетворять совокупности требований, предъявляемых к его функционированию, то есть функциональной спецификации. Такой проект будем называть правильным. Этот процесс занимает важную часть при проектировании, так как обнаружение любой некорректности в работе проекта после его реализации приводит к значительным затратам на ее. устранение. Поэтому, разработчики и исследователи в этой области всегда искали подходящие методы доказательства корректности функционирования' проекта.
В. настоящее. время существует три основных подхода к решению задачи проектирования аппаратных средств и доказательства их корректности:
автоматический синтез;
проектирование и проверка-корректности функционирования с помощью тестировать ее программной модели:
- формальное доказательство того, что проект соответствует
его функциональной.спецификации;
Первый подход создает по некоторому исходному описанию схему, состоящую из примитивных компонентов, поведение которых соответствует заданному. Такое проектирование будет, правильным, если примитивные компоненты были верифицированы перед тем. как они используются в создании схем, и правила преобразования, используемые для создания схем по исходному описанию были корректны. Этот подход считается самым привлекательным, но и самым трудным, и поэтому преждевременно говорить о наличии развитых методов автоматического синтеза проектов аппаратных средств ЭВМ
Второй подход, заключающийся в тестировании модели проектируемых аппаратных средств, является наиболее распространенным в настоящее время. Однако практически данный подход не может обеспечить доказательство полной правильности про-
- 2 -.
ектов из-за возрастающего количества вхддных наборов. Поэтому обычно проводится тестирование на ограниченном наборе входных воздействий, что снимает тем самым достоверность получаемых результатов.
Поэтому в последние годы было выполнено довольно много работ в' направлении создания и изучения различных теоретических моделей, методов доказательства и алгоритмов для проведения формальной верификации - проверки корректности проектов аппаратных средств ЭЁМ. Естественно, что вначале методы верификации аппаратных средств были построены на основе методов верификации программ - это та область, в которой исследования начались раньше. Однако область верификации аппаратных средств имеет свои . специфические чег^ты. которые должны быть отражены в создаваемых моделях. Одной из сймых важных черт является параллельное функционирование компонентов цифровых схем.
Модель взаимодействующих последовательных процессов CSP представляет собой модель работы параллельных систем. Процессы в CSP развиваются параллельно и взаимодействуют....как между собой, так и с окружением, то есть CSP включает модель параллелизма с передачей сообщений. Таким образом, CSP удовлетворяет основному требсванию. заданному областью верификации проектов аппаратных средств ЭВМ'- .
VHDL - язык описания аппаратуры сверхскоростных ИС является перспективным стандартом в области языков описания аппаратуры. Разработка этого языка вызвана тем, что до недавнего времени не существовало стандартного языка описания аппаратуры. Сведений об исчерпывающих средствах (как теоретических методах, так и практически работающих программных системах) верификации описаний не языке VHDL обнаружить.в литературе не удалось.
Целью работы состоит в исследовании модели CSP как средства описания проектов аппаратуры и развитие на этой основе метедов, алгоритмов и инструментальных средств доказательства корректности проектов аппаратуры.
Для достижения, поставленной цели в работе решались следующее задачи:' -- мсследоввяие требований, налагаемых областью описания,про-
ектов аппаратных средств, обеспеченных CSP;
исследование возможности моделирования VHDL-описаний на основе CSP-описаний для их дальнейшей верификации; ,-
сравнительный анализ существующих методов верификации CSP-описаний;
разработка метода верификации CSP-описаний, рассматриваемых как проекты аппаратных средств ЭВМ;. .
разработка алгоритма и экспериментальной программы, обеспечивающей проведение верификации проектов аппаратных
.средств ЭВМ.
.Методы исследования основаны на использовании понятий и методов теории параллельных систем, вычислительных структур, формальных языков и математической логики; в работе сочетается формальный и содержательный подходы.
Научная новизна исследования состоит в том, что:
- предложен способ верификации CSP-описаний проектов аппа
ратных средств ЭВМ. Отличие метода состоит в том. что за
1 счет сужения вида CSP-описаний. к которым применим метод, удалось добиться полиномиальной сложности анализа корректности взаимодействия компонентов. Метод выявляет состояния, в которых может возникать дедлок;
- предложено использование CSP' в качестве средства моделиро
вания ряда конструкций. языка описания аппаратуры VHDL для
их дальнейшей верификации.'
Практическую ценность работы , представляют алгоритм и Программа, разработанные на основе предложенного метода. Программа обеспечивает проведение верификации параллельных CSP-описаний проектов аппаратных средств.
Внедрение результатов работы. Теоретические и практические результаты использовались в госбюджетных НИР кафедры ВТ в 1992-1993 гг. Полученные результаты в настоящее время подготавливаются в рамках экспериментальной системы верификации цифровых схем для использования в учебном процессе кафедры вычислительной техники ГЭТУ.
Апробация работы. Основные положение диссертационной работы докладывались и обсуждались на следующих конференциях:
- 46-й областной конференции "Актуальные проблек-j развития
-4-.
радиотехники, электроники и связи" (г.Ленинград. 199І г.);-научно-технической конференции профессорско-преподавательского состава ГЭТУ им. В.И.Ульянова (Ленина) (г.Санкт-Петербург. 1993 г.). ;
Публикаций. По материалам диссертационной работы опубликовано 2 научных статьи и і тезис доклада на конференции.
Структура и обьем работы. Диссертационная работа.состоит из введения, четырех разделов с выводами, заключения, списка литературы, включающего 66 наименований, и 2 приложений.. Основная часть работы изложена на 139 страницах. Работа содержит 12 рисунков и 1 таблицу. -'
