Введение к работе
Актуальность проблемы. Интенсивное развитие средств вычислительной техники, повышение их производительности и увеличение степени интеграции проектируемых для них интегральных микросхем с возрастающей остротой ставит вопрос проверки корректности проектируемых аппаратных средств ЭВМ. Поскольку человек становится все больше зависим от вычислительных машин и других цифровых устройств, цена возможной ошибки в работе подобной системы становится неприемлемо высокой, а последствия такой ошибки - катастрофическими. В связи с этим становится понятен интерес исследователей к вопросам проверки правильности проектируемых устройств и значительный рост количества работ в этой области.
Проверить правильность разработки можно различными способами: макетированиемг тестированием, формальным доказательством. Сложность современных устройств вычислительной техники ограничивает применение макетирования лишь некоторыми специальными областями.
В настоящее время наиболее распространенным средством проверки правильности служит тестирование. Однако сложность современных цифровых устройств настолько высока, что провести исчерпывающее тестирование за разумное время не представляется возможным. С другой стороны, существующие способы уменьшения количества тестовых наборов вместо доказательства отсутствия ошибок в проектируемом устройстве показывают лишь, что на данном этапе ошибок не обнаружено. Кроме того, методы тестирования и генерации тестовых наборов обычно разрабатываются для -обнаружения определенных, хорошо известных классов ошибок. Высокая стоимость внесения изменений в налаженный производственный процесс вместе с упоминавшейся высокой ценой сбоя устройства в процессе эксплуатации заставляют искать средства установления правильности проектируемого устройства до запуска его в производство.
Таким средством выступает формальное доказательство правильности проекта, основанное на использовании различных математических преобразований. Формальное доказательство, позволяющее гарантировать правильность проектируемого устройства на некотором этапе проектирования, будем называть верификацией.
Возможности формального доказательства вызывают интерес не только в теоретическом плане; формальные методы оказали значительное влияние на разработку устройств с повышенными требованиями к надежности. Методы формальной верификации доказали свои преимущества и при использовании в коммерческих разработках, например, в производстве мате-
матического сопроцессора транспьютера Inmos TMS Т800.
Вместе с тем, практическое применение методов верификации в промышленности сдерживается рядом факторов, центральным из которых является сложность. Чрезвычайно высокая сложность процесса верификации сколько-нибудь значимых цифровых схем на практике сильно уменьшает теоретические преимущества верификации перед тестированием.
Одним из путей преодоления указанной проблемы является учет дополнительных ограничений, накладываемых предметной областью. Подобный учет позволяет иногда значительно снизить сложность решаемой задачи. Другой путь преодоления высокой вычислительной сложности методов формальной верификации состоит в применении современных высокопроизводительных параллельных вычислительных средств. Использование последовательных алгоритмов в вычислительных средствах с массовым параллелизмом зачастую не приносит выигрыша в производительности, а в ряде случаев даже снижает ее. Это вызвано накладными расходами на организацию взаимодействия между параллельными процессами или неудачной организацией' такого взаимодействия. Для эффективного применения указанных вычислительных средств необходимы соответствующие методы и алгоритмы, исследованию и разработке которых посвящена настоящая диссертационная работа.
Целью работы является исследование и разработка параллельных алгоритмов и эффективного метода формального доказательства корректности проектов аппаратных средств вычислительной техники. Для достижения поставленной цели в работе решались следующие задачи:
-исследование и сравнительный анализ существующих методов верификации проектов аппаратных средств вычислительной техники;
-разработка параллельного алгоритма верификации проектов аппаратных средств вычислительной техники на основе формальной графовой модели описания проекта;
- исследование причин, осложняющих процесс верификации, и разра
ботка алгоритма распараллеливания процесса верификации на основе анали
за спецификации проекта;
-разработка метода верификации временных свойств проектируемых аппаратных средств и анализ возможностей распараллеливания разработанного метода;
- разработка инженерной методики, обеспечивающей выполнение про
цедуры верификации проектов аппаратных средств вычислительной техники;
-разработка алгоритмов и экспериментальной программной системы,
обеспечивающей выполнение параллельной верификации проектов аппаратных средств вычислительной техники.
Методы исследования. Для решения поставленных задач в работе используются понятия и методы математической логики, теории вычислительных систем, теории графов, комбинаторики; в работе сочетаются формальный и содержательный подходы.
Научная новизна исследования состоит в том, что:
- предложен эффективный метод верификации временных свойств про
ектов аппаратных средств вычислительной техники, отличающийся от суще
ствующих методов полиномиальной сложностью и возможностью примене
ния временных диаграмм в качестве средства спецификации проекта. Выпол
нен анализ возможностей распараллеливания предложенного метода и полу
чена оценка сложности метода при параллельной реализации;
-предложен параллельный алгоритм функциональной верификации проектов аппаратных средств вычислительной техники. Алгоритм отличается удобством сопряжения с существующими средствами САПР и использованием естественного параллелизма в работе аппаратных средств, и основан на объединении графовой модели объекта проектирования и принципа обратного прослеживания;
- предложен алгоритм снижения сложности выполнения процедуры ве
рификации на основе анализа спецификации проекта и получены оценки вы
игрыша от применения предложенного алгоритма. Достоинством алгоритма
является возможность его эффективного применения и при последователь
ных вычислениях, при этом выигрыш достигается не за счет распараллелива-
ния# а за счет снижения сложности последовательно решаемых подзадач.
Практическую ценность работы представляют:
-обзор существующих методов верификации проектов аппаратных средств ЭВМ;
-разработанные алгоритмы, инженерная методика и экспериментальная программная система, обеспечивающие проведение параллельной верификации проектов аппаратуры ЭВМ.
Внедрение результатов работы. Основные теоретические и практические результаты работы использовались в госбюджетных научно-исследовательских работах, выполненных на кафедре вычислительной техники Санкт-Петербургского государственного электротехнического университета в 1994-1995гг. Разработанная программная система верификации используется в учебном процессе на кафедрах вычислительной техники СПб ГЭТУ и Чувашского государственного университета (г.Чебоксары).
Апробация работы. Основные положения диссертационной работы докладывались и обсуждались на следующих конференциях.:
- Международная научно-техническая конференция «Диагностика, информатика и метрология - 94» (г. Санкт-Петербург, 1994г.);'
-50-й и 51-й областные научно-технические конференции СПб НТО ЮС имени А.С.Попова (г. Санкт-Петербург, 1995-1996гг.).
Публикации. По материалам диссертационной работы опубликовано 5 печатных работ, из них 1 статья и 4 тезисов докладов на конференциях.
Структура и объем работы. Диссертационная работа состоит из введе
ния, четырех разделов с выводами, заключения, списка литературы, вклю
чающего 97 наименований, и 3 приложений. Основная часть работы изложе
на на 109 страницах машинописного текста. Работа содержит 28 рисунков и 7
таблиц. .