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