ИСТИНА

Верификацией называется анализ результата проектирования (RTL-модели или FPGA-прототипа микропроцессора) на соответствие предъявляемым к нему требованиям. Это крайне трудоемкая работа, на которую, по разным оценкам, тратится от 50 до 80% ресурсов, выделенных на разработку. Самым распространенным подходом к верификации является тестирование (simulation-based verification): на RTL-модель, исполняемую в симуляторе, подаются тестовые воздействия; выдаваемые моделью реакции проверяются (сравниваются с эталонными). Основная трудность тестирования связана с многомерным пространством состояний микропроцессора — следствием сложной микроархитектуры (конвейер, спекулятивное исполнение, многопоточность, многоядерность и т.п.). Микропроцессор — программно управляемое устройство; наиболее естественный способ воздействия на него — через программу. Исполняя команды, микропроцессор “движется” вдоль некоторой траектории в пространстве состояний, задействуя те или иные свои механизмы. Задача инженеров-верификаторов — создать множество тестовых программ, максимально полно покрывающих управляющую логику микропроцессора. Решение этой задачи невозможно без средств автоматизации — генераторов тестовых программ. Такие средства часто разрабатывают “с нуля” под конкретный микропроцессор: это требует немалых усилий и, кроме того, значительно усложняет их сопровождение (добавление новых команд, режимов работы и т.п.). В докладе рассматривается MicroTESK — инструмент автоматизации разработки генераторов тестовых программ. Особенностью инструмента является использование формальных спецификаций системы команд для настройки архитектурно независимой части генератора, так называемого ядра, под конкретную архитектуру. Таким образом, разработка генератора сводится к описанию синтаксиса и семантики команд, логики обработки исключений и управления памятью. В докладе на примере архитектуры MIPS разбирается процесс спецификации команд (язык nML) и подсистемы памяти (язык MMUSL), демонстрируются возможности инструмента по описанию шаблонов тестовых программ (язык Ruby, расширенный специальными конструкциями). Инструмент MicroTESK успешно применялся для верификации MIPS-совместимых микропроцессоров, разрабатываемых в НИИСИ РАН. Ядро инструмента, как и его версия для архитектуры MIPS, распространяется с открытым исходным кодом (open source) по лицензии Apache License v2.0.