Динамическая верификация цифровой аппаратуры на основе формальных спецификаций Чупилко Михаил Михайлович Научный руководитель проф., д.ф.-м.н. Петренко Александр Константинович Федеральное государственное бюджетное учреждение науки Институт системного программирования РАН

Фотошаблоны Эталонная модель на C++ Процесс создания аппаратуры 2/20 Документация HDL-описание (Verilog/VHDL) Микросхема Верификация HDL- симулятор Тестовая система Системный симулятор Системный симулятор

Причины сложности верификации аппаратуры Логическая сложность (параллелизм и асинхронность, большие размеры) Процесс разработки существенно итеративен, поэтому тесты и модели приходится многократно модифицировать Модульность проекта существенно слабее, чем в ПО, и изменения в одной подсистеме часто требуют корректировки в других Документация фрагментарная и часто не актуальная Постоянное увеличение сложности аппаратуры 3/20

Цель работы Разработка метода верификации цифровой аппаратуры на основе использования программных моделей с учетом требований промышленных процессов проектирования HDL-описаний 4/20

Поставленные задачи Проанализировать существующие методы верификации цифровой аппаратуры Разработать метод верификации HDL-описаний аппаратуры на основе использования эталонных программных моделей, поддерживающий: применение при неполноте требований инкрементальный процесс разработки и уточнения формальных спецификаций в процессе проектирования композицию тестовых систем различных HDL-описаний Разработать инструменты, реализующие метод Оценить реализацию метода на практике 5/20

Научная новизна Метод спецификации цифровой аппаратуры, подходящий для использования на разных уровнях абстракции Метод сопоставления реакций цифровой аппаратуры и реакций эталонной модели, позволяющий автоматизировать процедуру проверки цифровой аппаратуры 6/206/20

Существующие методы верификации HDL-описаний Формальная верификация (аналитическая верификация) Динамическая верификация (тестирование) Целевой объект: модуль (unit) / система в целом (core) Фаза генерации теста: в ходе статического анализа / в процессе исполнения Тестовые воздействия: случайные / набор / по ограничениям Оракул: наборы эталонных результатов / вычисление эталонных результатов по модели / ограничение на ожидаемый результат (post-условие) / контроль assertions Метрики полноты: по структуре HDL-описания / эталонной модели 7/20

Место предлагаемого метода Формальная верификация (аналитическая верификация) Динамическая верификация (тестирование) Целевой объект: модуль (unit) / система в целом (core) Фаза генерации теста: в ходе статического анализа / в процессе исполнения Тестовые воздействия: случайные / набор / по ограничениям Оракул: наборы эталонных результатов / вычисление эталонных результатов по модели / ограничение на ожидаемый результат (post-условие) / контроль assertions Метрики полноты: по структуре HDL-описания / эталонной модели 8/20 модуль (unit) в процессе исполнения случайные / набор / по ограничениям вычисление эталонных результатов по модели эталонной модели

Выделенные задачи как средство достижения поставленной цели Для быстрого получения тестов при неполных требованиях, обычных на ранних этапах проектирования аппаратуры: Поддержка эталонных C++ моделей с абстракцией времени и функциональности, отличной от HDL-описания Поддержка автоматизированных генераторов тестовых последовательностей Для экономии времени и затрат на верификацию на каждой следующей итерации проектирования HDL-описания: Средства доработки эталонных моделей до потактовых Использование эталонных моделей, которые дорабатываются в соответствии с каждой новой итерацией проектирования HDL-описания Средства расширения возможностей генераторов тестовой последовательности заданием режима обхода конечных автоматов Для учета декомпозиции как основного пути создания сложных HDL-описаний: Средства объединения тестовых систем различных HDL-описаний 9/209/20

Метод модульной верификации аппаратуры на основе моделей 10/20

Метод модульной верификации аппаратуры на основе моделей 11/20 применение при неполноте требований инкрементальный процесс разработки и уточнения формальных спецификаций в процессе проектирования композицию тестовых систем различных HDL-описаний

Разработанный метод модульной верификации аппаратуры 12/20

Формализация работы тестового оракула 13/20

Реализация метода. Библиотека C++TESK Hardware Edition Средства генерации стимулов Класс генератора тестовой последовательности, создающий случайный поток стимулов (взят из C++TESK) Класс генератора тестовой последовательности, создающий поток стимулов на основе обхода конечных автоматов (взят из C++TESK) Средства задания автоматной модели обобщенного состояния – набор макросов, реализующий класс тестового сценария (взят из C++TESK) Средства создания тестового оракула Классы сопоставителей реакций Класс генератора вердикта Средства описания окружений эталонной модели – набор макросов, реализующий класс описания окружения Подключение к HDL-описанию Средства описания адаптеров HDL-описаний – набор макросов, реализующий класс адаптера 14/20

15/20 Применение метода в реальных проектах Библиотека классов C++TESK Hardware Edition была применена для создания тестовых систем для 9 уже верифицированных модулей микропроцессоров в течение гг., в среднем обнаруживалось по 3-5 серьезных ошибок: Буфер трансляции адресов (НИИСИ) Модуль арифметики с плавающей точкой (НИИСИ) Кэш память второго уровня (НИИСИ) Коммутатор данных (МЦСТ) Системный контроллер прерываний (МЦСТ) Модуль доступа к памяти (МЦСТ) Устройство аппаратного поиска по таблице страниц (МЦСТ) Контроллер банка кэш-памяти второго уровня (МЦСТ) Буфер команд (МЦСТ)

Результаты применения метода в реальных проектах 16/20

Сравнение результатов с традиционным подходом 17/20

Апробация и публикации SYRCoSE: Spring Young Researches Colloquium on Software Engineering, г. Нижний Новгород, 2010 г. и г. Екатеринбург, 2011 г. EWDTS: East-West Design & Test Symposium, г. Санкт-Петербург, 2010 г. и г. Севастополь, 2011 г. Baltic Electronics Conference, г. Таллин, 2010 г. Семинар Института системного программирования РАН, г. Москва, гг. По теме диссертации автором опубликовано 11 работ (из них 3 в изданиях по перечню ВАК) 18/20

Заключение Разработан метод верификации цифровой аппаратуры, на основе формальных спецификаций в виде программных моделей на языке C++, отвечающий требованиям промышленных процессов проектирования HDL-описаний Разработан метод спецификации цифровой аппаратуры, подходящий для использования на разных уровнях абстракции Разработан метод сопоставления реакций цифровой аппаратуры и реакций эталонной модели, позволяющий автоматизировать процедуру проверки цифровой аппаратуры Реализованы инструменты, поддерживающие разработанные методы Реализация методов была применена на практике для тестирования модулей сложных отечественных микропроцессоров 19/20

Спасибо Вопросы?