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


Генератор тестовых программ MicroTESK: средства моделирования системы команд микропроцессорах

Андрей Татарников. Начало семинара - 16 апреля 2013 г.

Основной метод функциональной верификации микропроцессоров - генерация и выполнение тестовых программ. Несмотря на доступные на рынке мощные автоматические генераторы, создание тестов требует серьёзных усилий и временных затрат и значительно удлиняет цикл разработки дизайна микропроцессора. Главная проблема состоит в том, что большинство существующих средств разработано под конкретную архитектуру и для их адаптации к новой архитектуре или к изменениям в текущей приходится переписывать значительную часть их кода. Чтобы решить эту проблему, MicroTESK использует подход, в котором генератор разделён на две части: (1) модель архитектуры, содержащую знание о конкретном микропроцессоре, и (2) ядро генератора, реализующее общую для всех микропроцессоров логику генерации. Данный подход был предложен ещё в 90-е годы IBM Research и реализован в инструменте Genesys-Pro. Однако у их инструмента есть существенный недостаток: процесс создания моделей остается трудоёмким и требует специальных навыков, которыми инженер-верификатор, как правило, не обладает. MicroTESK предлагает упростить эту задачу путём использования высокоуровневых формальных спецификаций, которые автоматически транслируются в модель архитектуры на языке Java. Текущая версия использует для описания системы команд язык Sim-nML. Данный язык по своему синтаксису схож с псевдокодом, используемом в справочных руководствах для описания семантики команд микропроцессора. Такой подход значительно сокращает усилия, требуемые для создания модели, и позволяет инженерам-верификаторам быстро адаптировать генератор тестов к изменениям в дизайне микропроцессора.

С презентацией доклада можно ознакомиться здесь.

Семинар группы

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

Перейти к списку семинаров ИСП РАН