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

Андрей Татарников. Начало семинара - 12 марта 2014 г.

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

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

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

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

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