Институт системного программирования им. В.П. Иванникова РАН


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

Авторы

М.М.Чупилко.

Аннотация

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

Полный текст статьи в формате pdf

Издание

Диссертация на соискание ученой степени к.ф.-м.н., Москва, 2012 г.

Научная группа

Технологии программирования

Все публикации за 2012 год Все публикации