Электронная библиотека Веда
Цели библиотеки
Скачать бесплатно
Доставка литературы
Доставка диссертаций
Размещение литературы
Контактные данные
Я ищу:
Библиотечный каталог российских и украинских диссертаций

Вы находитесь:
Диссертационные работы России
Технические науки
Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Диссертационная работа:

Чупилко Михаил Михайлович. Динамическая верификация цифровой аппаратуры на основе формальных спецификаций: автореферат дис. ... кандидата физико-математических наук: 05.13.11 / Чупилко Михаил Михайлович;[Место защиты: Институте системного программирования РАН].- Москва, 2012.- 24 с.

смотреть введение
Введение к работе:

Актуальность темы

Современная цифровая аппаратура на основе интегральных схем (ИС) представляет собой сложные устройства, проектирование и производство которых требует больших затрат ресурсов. Непосредственное изготовление ИС происходит с использованием наборов фотошаблонов, которые создаются на основе схемы соединений (net list). Схема соединений получается автоматически путем синтеза из модели, созданной на специализированном языке описания аппаратуры. В настоящее время проектирование моделей устройств осуществляется с помощью языков, называемых языками описания аппаратуры {Hardware Description Language, HDL). Такие модели, основанные на HDL-описаниях, часто называют имитационными, так как они допускают их выполнение в специализированной среде имитационного моделирования -симуляторе.

Цена ошибки в аппаратуре может оказаться очень высокой: известный случай замены микропроцессоров Intel Pentium с ошибкой деления обошелся компании приблизительно в 500 миллионов долларов (Wolfe A. For Intel, it's а case of FPU all over again. ЕЕ Times, 1997. №5). Так как исправление ошибок в уже готовых микросхемах невозможно, поиск и нахождение функциональных ошибок проводится на этапе проектирования HDL-описания устройства. Подобного рода деятельность, состоящая в проверке соответствия поведения аппаратуры, задаваемого HDL-описанием, его спецификации, называется верификацией. Верификация обычно требует до 70% от общих трудозатрат на создание всего устройства. Это обусловлено следующими причинами: логической сложностью HDL-описаний и ее постоянным увеличением (высокая степень параллелизма, асинхронность и большие размеры), существенной итеративностью процесса разработки HDL-описаний, требующего постоянной модификации тестов и HDL-описаний, меньшим уровнем модульности, чем в

области программного обеспечения, фрагментарностью и неактуальностью документации.

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

Традиционный метод динамической верификации состоит в следующем. Набор входных данных для проведения верификации {тестовая последовательность) описывается вручную или генерируется случайным образом, но в рамках ограничений, наложенных на значения отдельных элементов последовательности. Собственно проверка корректности поведения, задаваемого HDL-описанием, оценивается на основе утверждений (assertions), а для оценки полноты верификации используются метрики на основе покрытия кода HDL-описания и покрытия комбинаций событий, возникающих в процессе выполнения HDL-описания в симуляторе (Open Verification Methodology User Guide [Электронный ресурс], 2011. URL: ).

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

фрагментарности проверяемых свойств, от чего также страдает качество верификации.

Решению задачи тщательного тестирования HDL-описаний посвящено много работ. Многие из проблем, перечисленных выше, решены, например, в методе верификации HDL-описаний, основанном на формальных спецификациях, описывающих ожидаемое поведение тестируемой аппаратуры, в форме программных контрактов, наложенных на все операции и микрооперации (Камкин, А.С. Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций, диссертация на соискание ученой степени кандидата физико-математических наук. М., 2009). Такие спецификации описывают ожидаемое поведение с потактовой точностью. Верификация в этом случае получается очень тщательной, так как вердикт касательно корректности HDL-описания выносится на основе и проверки данных, и проверки номера такта, на котором выполняемое в симуляторе HDL-описание выдало реакцию. Детальная документация, равно как и необходимость в столь тщательных проверках, появляется, как правило, на заключительных итерациях создания HDL-описаний, поэтому наилучшее применение метод нашел именно на них. Требования метода к документации, а также сложность разработки спецификаций сделали его применение ограниченным: разработка потактовых спецификаций, которые к тому же не используют разработанные ранее на предыдущих этапах эталонные модели, занимает много ресурсов и времени, которых может и не остаться на заключительных итерациях проектирования.

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

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

Цель и задачи работы

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

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

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

применение при неполноте требований;

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

композицию тестовых систем различных HDL-описаний;

  1. Разработать инструменты, реализующие метод;

  2. Оценить реализацию метода на практике.

Научная новизна работы

Научной новизной обладают следующие результаты работы:

  1. Метод спецификации цифровой аппаратуры, подходящий для использования на разных уровнях абстракции;

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

Практическая значимость

На основе предложенного метода верификации были разработаны средства, позволяющие создавать тестовые системы на основе эталонных моделей на C++ на разных уровнях абстракции. Разработанные средства являются библиотекой классов на языке C++. Они были применены в 9 проектах верификации модулей промышленных микропроцессоров в течение 2009-2012 гг. В процессе верификации в среднем обнаруживалось 3-5 серьезных ошибок в модулях, прошедших верификацию другими методами. Продемонстрированы преимущества метода для поддержки итеративного процесса разработки.

Доклады и публикации

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

Весенний коллоквиум молодых исследователей в области программной инженерии (SYRCoSE: Spring Young Researchers Colloquium on Software Engineering, г. Нижний Новгород, 2010 г. и г. Екатеринбург, 2011 г.);

Международный симпозиум «Восток-Запад: проектирование и тестирование» (EWDTS: East-West Design & Test Symposium, г. Санкт-Петербург, 2010 г. и г. Севастополь, 2011 г.);

Международная конференция «Балтийская электронная конференция» (Baltic Electronics Conference, г. Таллин, 2010 г.);

Семинар Института системного программирования РАН (г. Москва, 2011-2012 гг.).

По теме диссертации автором опубликовано 11 работ (из них 3 в изданиях из перечня ВАК), список которых приведен в конце автореферата.

Структура и объем диссертации


© Научная электронная библиотека «Веда», 2003-2013.
info@lib.ua-ru.net