Автоматизация конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат наук Татарников Андрей Дмитриевич

• Татарников Андрей Дмитриевич
• кандидат наук
• 2017

Оглавление диссертации кандидат наук Татарников Андрей Дмитриевич

Введение

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

1.1 Проектирование микропроцессоров

1.2 Функциональная верификация микропроцессоров

1.3 Техники генерации тестовых программ

1.4 Инструменты генерации тестовых программ

1.4.1 Инструменты НИИСИ РАН

1.4.2 Инструменты ARM

1.4.3 Инструменты IBM Research

1.4.4 Разработки ИСП РАН

1.4.5 Другие разработки

1.5 Выводы

Глава 2. Автоматизация конструирования генераторов тестовых программ

2.1 Метод автоматизации конструирования генераторов тестовых программ

2.1.1 Использование формальных спецификаций

2.1.2 Описание архитектуры микропроцессора на языке nML

2.1.3 Расширение возможностей языка nML

2.1.4 Архитектура модели микропроцессора

2.2 Язык описания шаблонов тестовых программ

2.2.1 Структура тестовых программ

2.2.2 Описываемые свойства тестовых программ

2.2.3 Концепция языка описания шаблонов тестовых программ

2.2.4 Описание последовательностей команд

2.2.5 Описание правил выбора регистров

2.2.6 Описание тестовых ситуаций

2.2.7 Описание инициализирующего кода и встроенных проверок

2.2.8 Описание правил рандомизации

2.2.9 Описание размещения команд и данных в памяти

2.2.10 Описание структуры переходов между тестовыми примерами

2.2.11 Расширяемость языка описания шаблонов тестовых программ

2.3 Архитектура генераторов тестовых программ

2.3.1 Анализатор шаблонов тестовых программ

2.3.2 Обработчик внутреннего представления

2.3.3 Итератор последовательностей команд

2.3.4 Обработчик последовательностей команд

2.3.5 Расширяемость генератора тестовых программ

2.4 Выводы

Глава 3. Реализация предложенного метода

3.1 Среда моделирования

3.1.1 Модель микропроцессора

3.1.2 Анализаторы формальных спецификаций

3.1.3 Генераторы кода и библиотеки моделирования

3.2 Среда тестирования

3.2.1 Анализатор шаблонов тестовых программ

3.2.2 Внутреннее представление шаблонов тестовых программ

3.2.3 Обработчик внутреннего представления

3.2.4 Итератор последовательностей команд

3.2.5 Распределитель регистров

3.2.6 Обработчик последовательностей команд

3.2.7 Исполнитель последовательностей команд

3.2.8 Генератор данных

3.2.9 Построитель встроенных проверок

3.3 Расширяемость инструмента MicшTESK

3.4 Выводы

Глава 4. Результаты практического применения

4.1 Генератор тестовых программ для архитектуры MIPS64

4.1.1 Архитектура М1РБ64

4.1.2 Спецификации архитектуры MIPS64

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

4.2 Генератор тестовых программ для архитектуры ARMv8

4.2.1 Архитектура ARMv8

4.2.2 Спецификации архитектуры ARMv8

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

4.2.4 Проверка корректности генерируемых тестовых программ

4.3 Генератор тестовых программ для архитектуры PowerPC

4.3.1 Архитектура PowerPC

4.3.2 Спецификации архитектуры PowerPC

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

4.4 Генератор тестовых программ для архитектуры RISC-V

4.4.1 Архитектура RISC-V

4.4.2 Спецификации архитектуры RISC-V

4.4.3 Генерация тестовых программ для архитектуры RISC-V

4.5 Выводы

Заключение

Список литературы

Приложения

Введение

Введение диссертации (часть автореферата) на тему «Автоматизация конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций»

Актуальность темы

Микропроцессоры [16] лежат в основе большинства электронных устройств. В то время как другие компоненты отвечают за ввод и вывод данных, роль микропроцессора состоит в обработке этих данных: он определяет, какие операции должны быть выполнены над данными и контролирует процесс их выполнения. Микропроцессоры состоят из множества транзисторов, объединенных в единый вычислительный элемент на полупроводниковом кристалле. Число транзисторов увеличивается по закону Мура [17] и в настоящее время достигает нескольких миллиардов [18] (см. рисунок 1).

Рисунок 1. Рост числа транзисторов (на графике — десятичный логарифм) в микропроцессорах компании

Intel

Высокая сложность современных микропроцессоров, вызванная оптимизацией производительности и энергопотребления, приводит ошибкам проектирования. Дальнейшее усложнение влечет за собой рост числа ошибок. Например, по данным на август 2008-го года в микропроцессоре Intel Pentium 4 было найдено 104 ошибки, из которых 43 не исправлено и их исправление не запланировано [19]. В то же время в микропроцессоре Intel Core i7-900 по данным на февраль 2015-го года обнаружено 167 ошибок, из которых исправлено только 16 и еще для 2 запланировано исправление [20]. Следует понимать, что в обоих случаях речь идет лишь об известных проблемах, в то время как реальное число ошибок может быть гораздо выше.

5

Цена ошибок в микропроцессорах очень высока. В отличие от дефектов в программах, которые устраняются сравнительно просто, ошибки в микропроцессорах не могут быть исправлены и для их устранения потребуется повторный выпуск и замена микросхемы или целого блока. Например, в 1994-м году замена продукции из-за ошибки в реализации команды FDIV микропроцессора Pentium обошлась компании Intel в 475 миллионов долларов [21].

Обеспечение функциональной корректности микропроцессоров является фундаментальной проблемой, для решения которой применяется комплекс мер, известный как функциональная верификация. Она выполняется параллельно с проектированием, и ее задача заключается в проверке соответствия результатов, полученных на текущем этапе, заданным требованиям и ограничениям. Верификация является весьма трудоёмкой задачей. По некоторым оценкам, затраты на нее достигают 70-80% от общих затрат на проектирование, а число инженеров-верификаторов примерно вдвое превосходит число инженеров-разработчиков [22]. С ростом сложности микропроцессоров ситуация только ухудшается — возможности методов верификации отстают от развития микропроцессоров; соответственно, проверка корректности (и без того являющаяся самым узким местом процесса проектирования) вовлекает в себя все большие объемы ресурсов. Таким образом, задача совершенствования методов и инструментов верификации имеет ключевое значение.

Наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является имитационная верификация (simulation-based verification), также называемая тестированием. На системном уровне (т.е. на уровне устройства в целом) она осуществляется следующим образом: создаются тестовые программы на языке ассемблера; программы запускаются на проектной модели микропроцессора; в результате получаются трассы исполнения, содержащие информацию о событиях, которые

произошли в процессе исполнения программ; полученные трассы проверяются на корректность.

Создание тестовых программ осуществляется при помощи специальных программных инструментов, известных как генераторы тестовых программ. Они используют различные техники генерации для обеспечения максимальной полноты тестирования: от случайной генерации до нацеленной генерации, основанной на формальных методах. Ни одна из них не является универсальным решением для всех задач верификации, поэтому на практике применяется множество дополняющих друг друга техник. Общепринятым подходом является генерация на основе шаблонов тестовых программ, описывающих структурные и поведенческие свойства программ. Обработка тестового шаблона состоит в применении той или иной техники генерации для удовлетворения того или иного свойства.

Как правило, генераторы тестовых программ предназначены для конкретных микропроцессорных архитектур и основаны на конкретных техниках генерации. Однако, так как микропроцессорные архитектуры и техники генерации эволюционируют, возникает задача расширения возможностей существующих генераторов. Трудность ее решения заключается в том, что знание об архитектуре микропроцессора зачастую неотделимо от реализации техник генерации. Поддержка новых архитектур и техник генерации требует существенных изменений в реализации генератора. Чтобы этого избежать, инженеры-верификаторы вынуждены одновременно использовать несколько генераторов, каждый из которых решает какую-то отдельную задачу. При этом совместное использование различных техник генерации для решения общей задачи оказывается невозможным.

Таким образом, актуальной является задача разработки метода, позволяющего создавать для любых микропроцессорных архитектур генераторы тестовых программ, интегрирующие в себе разные техники генерации. Перспективным решением данной задачи видится автоматизированное конструирование генераторов тестовых программ на

основе формальных спецификаций архитектуры микропроцессора. При этом формальные спецификации будут выступать в качестве источника знания об архитектуре тестируемого микропроцессора, используемого компонентами генератора, реализующими техники генерации. Генерация будет осуществляться на основе шаблонов, разработанных на специальном языке, позволяющем описывать свойства тестовых программ в терминах формальных спецификаций и задавать техники генерации, применяемые для удовлетворения этих свойств.

Цель и задачи работы

Цель работы — разработка метода автоматизации конструирования генераторов тестовых программ для микропроцессоров. Метод должен быть применимым к широкому спектру микропроцессорных архитектур. Генераторы должны создавать тестовые программы на языке ассемблера по шаблонам, описывающим структурные и поведенческие свойства этих программ. Генераторы должны реализовывать разные техники генерации и быть расширяемыми. Для достижения цели работы были поставлены следующие задачи:

1. Провести анализ существующих методов и средств генерации тестовых программ для микропроцессоров.

2. Разработать метод автоматизации конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций.

3. Разработать язык описания шаблонов тестовых программ, позволяющий описывать их структурные и поведенческие свойства.

4. Разработать архитектуру расширяемого генератора тестовых программ для микропроцессоров, позволяющую интегрировать разные техники генерации.

5. Разработать программный инструмент, реализующий предложенный метод автоматизации конструирования генераторов тестовых программ.

6. Оценить характеристики предложенного метода на основе опыта

применения разработанного программного инструмента для

8

конструирования генераторов тестовых программ для нескольких микропроцессорных архитектур.

Научная новизна работы

Научной новизной обладают следующие результаты работы:

1. Метод автоматизации конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций.

2. Язык описания шаблонов тестовых программ, позволяющий описывать их структурные и поведенческие свойства.

3. Архитектура генератора тестовых программ для микропроцессоров, позволяющая интегрировать разные техники генерации.

Теоретическая и практическая значимость

В работе предложен метод автоматизации конструирования генераторов тестовых программ для микропроцессоров. В основе предложенного метода лежат архитектурно-независимые техники генерации, для применения которых к конкретной микропроцессорной архитектуре используется информация, полученная в результате анализа формальных спецификаций этой архитектуры. Результаты проведенного исследования могут послужить основой для разработки архитектурно-независимых техник генерации тестовых программ и создания программных инструментов, основанных на анализе формальных спецификаций. Кроме этого, эти результаты могут использоваться в исследовательских проектах и учебных курсах по проектированию и верификации микропроцессоров.

На основе предложенного метода разработан программный инструмент MicroTESK, позволяющий автоматизировать на основе формальных спецификаций конструирование генераторов тестовых программ для микропроцессоров. Разработанный инструмент был применен для создания генераторов тестовых программ для архитектур MIPS64, ARMv8, PowerPC и RISC-V. Генераторы тестовых программ для MIPS64 и ARMv8 используются в отечественных и зарубежных компаниях. Помимо этого, разработанный

инструмент может быть использован для создания генераторов тестовых программ для широкого спектра других микропроцессорных архитектур.

Методология и методы исследования

Методологическую основу исследования составляют теория компиляторов, теория формальных языков, теория автоматов, теория множеств, теория графов, теория алгоритмов и математическая логика.

Положения, выносимые на защиту

1. Метод автоматизации конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций.

2. Язык описания шаблонов тестовых программ, позволяющий описывать их структурные и поведенческие свойства.

3. Архитектура генераторов тестовых программ для микропроцессоров, позволяющая интегрировать разные техники генерации и допускающая расширение множества поддерживаемых техник.

4. Программный инструмент, использующий предложенный метод для конструирования генераторов тестовых программ с предложенной архитектурой, осуществляющих генерацию на основе шаблонов на предложенном языке.

Апробация работы

Основные положения работы обсуждались на следующих конференциях и семинарах:

• Международная конференция «Design Automation Conference», выставка University Booth (г. Остин, США, 2-7 июня 2013 г. и г. Сан-Франциско, США, 2-5 июня 2014 г.);

• Международная конференция «Design, Automation & Test in Europe», выставка University Booth (г. Гренобль, Франция, 18-22 марта 2013 г.; г. Дрезден, Германия, 24-28 марта 2014 г.; г. Гренобль, Франция, 10-12 марта 2015 г.; г. Лозанна, Швейцария, 28-30 марта 2017 г.);

• Международный коллоквиум молодых исследователей в области программной инженерии «Spring/Summer Young Researchers' Colloquium on Software Engineering» (г. Пермь, 30-31 мая 2012 г. и д. Красновидово, 30 мая-1 июня 2016 г.);

• Международная конференция «A.P. Ershov Informatics Conference» (г. Москва, 27-29 июня 2017 г.);

• Открытая конференция ИСП РАН (г. Москва, 1-2 декабря 2016 г.);

• Международный симпозиум «IEEE East-West Design & Test Symposium» (г. Ереван, Армения, 14-17 октября 2016 г.);

• Всероссийская научно-техническая конференция «Проблемы разработки перспективных микро- и наноэлектронных систем» МЭС-2016 (г. Москва, 3-7 октября 2016 г.);

• Международная конференция «Новые информационные технологии в исследовании сложных структур» (г. Екатеринбург, 6-10 июня 2016 г.);

• Международная летняя школа молодых ученых «Новые информационные технологии в исследовании сложных структур» (г. Анапа, 8-12 июня 2015 г.);

• Научно-техническая конференция студентов, аспирантов и молодых специалистов НИУ ВШЭ им. Е.В. Арменского (г. Москва, 4 февраля 2015 г.);

• Совместный семинар ЗАО «МЦСТ» и ИСП РАН «Проблемы верификации микропроцессоров» (г. Москва, 10 апреля 2014 г.);

• Семинар Института системного программирования РАН (г. Москва, 2013, 2014 и 2016 гг.).

Публикации

По теме диссертации автором опубликовано 15 работ, в том числе 7 научных статей [1-7] в рецензируемых журналах, входящих в перечень журналов, рекомендованных ВАК РФ. В работе [2] автором описывается архитектура инструмента MicroTESK. В статье [5] вклад автора заключается в

описании средств системной верификации микропроцессоров. В работах [6, 14] автору принадлежит описание концепции и архитектуры расширяемой среды генерации тестовых программ. В работах [7, 10, 11] вклад автора состоит в разработке средств моделирования подсистемы памяти и конструкций языка описания шаблонов тестовых программ, позволяющих создавать тесты на подсистему памяти. В работе [13] автором дается обзор существующих подходов и формулируются требования к системе хранения информации, используемой для построения тестов. В статье [15] автором описываются предлагаемый подход к моделированию архитектуры микропроцессора и концепция языка описания шаблонов тестовых программ.

Личный вклад

Все представленные в диссертации результаты получены лично автором.

Структура и объем диссертации

Работа состоит из введения, четырех глав, заключения, списка литературы (122 наименования) и одного приложения. Основной текст диссертации (без списка литературы и приложения) занимает 148 страниц.

Краткое содержание диссертации

Во введении обосновывается актуальность темы работы, определяются ее цели и задачи, раскрывается теоретическая и практическая значимость.

Первая глава содержит обзор подходов к функциональной верификации микропроцессоров. Основное внимание уделяется верификации при помощи тестовых программ. В главе рассматриваются сильные и слабые стороны распространенных техник генерации тестовых программ, области их применения и варианты их совместного использования. Также делается сравнительный анализ возможностей существующих инструментов, реализующих эти техники. На основе данного анализа делается вывод об отсутствии генератора тестовых программ, который был бы применим для широкого спектра микропроцессорных архитектур и позволил бы

интегрировать основные применяемые на практике техники генерации, и выдвигается тезис об актуальности задачи его создания.

Во второй главе предлагается метод автоматизации конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций их архитектуры. Данный метод предполагает, что информация, извлеченная из формальных спецификаций, будет использоваться для обеспечения целенаправленности тестирования и контроля состояния микропроцессора в процессе генерации. Построение тестовых программ будет осуществляться на основе шаблонов, разработанных на специальном расширяемом языке, позволяющем описывать их структурные и поведенческие свойства. Расширяемая архитектура генераторов позволит интегрировать разные техники генерации. Глава состоит из трех разделов, в которых описывается предлагаемый метод автоматизации конструирования генераторов тестовых программ, язык описания шаблонов тестовых программ и архитектура конструируемых генераторов тестовых соответственно.

В третьей главе описывается реализация предложенного метода автоматизации конструирования генераторов тестовых программ. Метод нашел свое воплощение в инструменте с открытым исходным кодом MicroTESK (Microprocessor TEsting and Specification Kit) версии 2.0, разработанном на языке Java. Данный инструмент на основе формальных спецификаций конструирует генераторы тестовых программ, состоящие из модели микропроцессора и архитектурно-независимого ядра. Глава состоит из двух разделов, в которых описывается реализации инструмента MicroTESK и реализация архитектурно-независимого ядра генераторов тестовых программ соответственно.

В четвертой главе описываются результаты применения предложенного метода автоматизации конструирования генераторов тестовых программ для микропроцессоров MIPS64, ARMv8, PowerPC и RISC-V. В главе оценивается трудоемкость создания генераторов с применением предложенного метода и приводится сравнение с результатами применения других аналогичных

методов. Также в главе обосновывается применимость предложенного метода для конструирования генераторов тестовых программ для микропроцессорных архитектур промышленного масштаба.

В заключении перечисляются основные результаты работы.

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

Данная глава содержит обзор техник и инструментов, применяемых для генерации тестовых программ для функциональной верификации микропроцессоров. В начале главы рассказывается об области применения генераторов тестовых программ, а затем делается сравнительный анализ существующих техник и инструментов. На основе данного анализа формулируется основные требования к методу автоматизации конструирования генераторов тестовых программ, предлагаемому в данной работе.

1.1 Проектирование микропроцессоров

Проектирование микропроцессора - сложный процесс, включающий в себя нескольких этапов [16, 25, 26], на каждом из которых создается описание микропроцессора на определенном уровне абстракции. На рисунке 2 показана общая схема процесса проектирования микропроцессора.

Проектирование микропроцессора начинается с составления детального плана (технического задания), в котором описывается концепция проектируемого устройства, целевая рыночная ниша и основные

/х

План

Спецификации

Рисунок 2. Процесс проектирования микропроцессора

характеристики (такие как цена, производительность и энергопотребление). Также определяется на основе каких предыдущих разработок будет создан микропроцессор и какое программное обеспечение будет на нем запускаться. Помимо этого делается оценка времени и ресурсов, отведенных на проектирование, составляется график работ и выбирается общая методология проектирования.

На этапе проектирования архитектуры определяется, какие команды будут поддерживаться микропроцессором. На этом этапе уточняются требования и создается спецификация архитектуры. Помимо документов требований и спецификаций архитектуры результатом данного этапа является программный эмулятор (симулятор), позволяющий интерпретировать программы, написанные для целевого микропроцессора. Он может использоваться для кросс-разработки программного обеспечения или выступать в качестве эталонной модели.

После архитектуры проектируется микроархитектура. Она описывает функциональные модули микропроцессора, их взаимодействие и разделение задач между ними. На этом этапе определяются такие характеристики, как организация конвейера команд и иерархии памяти, способ реализации многопоточности и т.д. Обычно результатом проектирования микроархитектуры являются диаграммы взаимодействия между модулями и спецификации, описывающие различные алгоритмы. Кроме того на этапах проектирования архитектуры и микроархитектуры осуществляется моделирование. Для этого применяются следующие средства: (1) языки программирования общего назначения, (2) языки системного проектирования (SLDL, System-Level Design Languages) и (3) языки описания архитектуры (ADL, Architecture Description Languages) [27, 28, 29]. Примеры языков указанных типов представлены в таблице 1. С их помощью создаются модели для проведения различных экспериментов (например, программные эмуляторы или формальные модели), а также средства разработки для проектируемой архитектуры (компиляторы, дизассемблеры, и т.д.).

Тип языка Примеры

Языки программирования общего назначения C, C++, Perl, Python

Языки описания архитектуры (ADL) LISA, EXPRESSION, ISDL, nML

Языки системного проектирования (SLDL) SystemC, SystemVerilog, Bluespec

Языки описания аппаратуры (HDL) Verilog, VHDL

На следующем этапе при помощи языков описания аппаратуры (HDL, Hardware Description Languages) описывается логическая структура микропроцессора. Результатом данного этапа является модель уровня регистровых передач (RTL, Register Transfer Level), называемая также HDL-моделью или HDL-описанием, которая с потактовой точностью определяет пересылки данных, возникающие при работе устройства. На этапе разработки HDL-модели часто прибегают к прототипированию (prototyping) [30]. Оно предполагает создание функционально идентичной реализации, выполненной с использованием программируемых логических интегральных схем (ПЛИС), с целью проведения различных экспериментов.

После этого на основе HDL-модели строится функционально ей эквивалентная схема из логических вентилей в заданном технологическом базисе. Процесс построения данной схемы осуществляется средствами систем автоматизированного проектирования (САПР) и называется логическим синтезом.

Далее осуществляется построение топологии, которая описывает размещение транзисторов и проводников в слоях материала, их которого изготовляется схема на кристалле. Этот этап называется физическим синтезом и он, также как и логический синтез, автоматизирован средствами САПР. В результате получается представление (как правило, основанное на фотошаблонах), которое затем используется при производстве интегральных схем.

По завершению физического проектирования осуществляется выпуск (tape-out) первого опытного образца (first silicon) интегральной схемы. Данный образец проходит несколько циклов отладки, в процессе которых выявляются и

исправляются ошибки, перед тем как, созданный микропроцессор может быть выпущен на рынок.

1.2 Функциональная верификация микропроцессоров

Параллельно с процессом проектирования осуществляется контроль корректности полученных результатов. Для обеспечения функциональной корректности микропроцессоров применяется комплекс мер, известный как функциональная верификация. Прежде всего, эти меры нацелены на обнаружение и исправление ошибок, допущенных в процессе проектирования. Хотя функциональная верификация присутствует на всех этапах, особенно она актуальна при создании HDL-модели, поскольку функциональность, описанная на этом этапе, впоследствии не изменяется [26]. Верификация может осуществляться как на уровне отдельных модулей микропроцессора (модульная верификация), так и для устройства в целом (системная верификация).

Существуют два основных подхода к функциональной верификации: (1) имитационная верификация (simulation-based verification), также называемая тестированием, и (2) формальная верификация (formal method-based verification) [31]. Первый заключается в проверке корректности реакции проектируемого устройства, работа которого имитируется при помощи программного или аппаратного эмулятора, на тестовые воздействия. Второй основан на построении математической (формальной) модели и проверке выполнимости ее свойств. Формальная верификация позволяет осуществить исчерпывающую проверку всех возможных вариантов поведения, заданных моделью. Однако она имеет ряд ограничений (высокая трудоемкость и вычислительная сложность, а также трудности формализации), которые затрудняют ее использование в промышленных проектах. По этой причине на практике основной акцент делается на тестирование [32].

Тестирование микропроцессоров на системном уровне осуществляется

путем генерации тестовых программ на языке ассемблера, которые

представляют собой последовательности команд (инструкций)

микропроцессора, и анализа результатов их выполнения с целью убедиться, что

18

их поведение соответствует спецификации. Такой подход видится наиболее естественным, т.к. система команд определяет функциональность микропроцессора и является единственным доступным интерфейсом, через который пользователи могут с ним взаимодействовать. Верификация при помощи тестовых программ применима на всех этапах проектирования, начиная с момента создания программного эмулятора, но на каждом этапе имеет свои особенности, связанные со скоростью выполнения программ и уровнем детализации полученных результатов. В таблице 2 показаны примерная скорость выполнения тестов и уровень детализации результатов на различных прототипах [33]. Обычно тестирование начинается с HDL-модели и продолжается до выпуска продукции.

Таблица 2. Скорость выполнения тестов и уровень детализации результатов на различных прототипах

Объект тестирования Скорость выполнения (инстр./сек.) Уровень детализации

HDL-эмулятор 103 Очень высокая

Эталонный эмулятор на C/C++ 3 * 106 Высокая

ПЛИС-прототип 107 Средняя

Опытный образец микропроцессора 108 - 109 Очень низкая

Существуют два основных подхода к функциональной верификации микропроцессоров при помощи тестовых программ: (1) сравнение трасс выполнения с эталонными трассами и (2) использование встроенных проверок (self-checks).

Рисунок 3. Тестирование посредством сравнения трасс

В первом случае (см. рисунок 3) при выполнении программы на HDL-модели или другой программной модели создается трасса выполнения, фиксирующая события, которые происходят в микропроцессоре. Полученная трасса сравнивается с эталонной трассой, полученной в результате выполнения той же программы на эталонной модели (reference model). Для сравнения трасс используются специальные программы, называемые компараторами.

19

Эталонная модель создается независимо от HDL-модели на языке высокого уровня (например, C или C++) и является более абстрактной. Часто в качестве эталонной модели выступает эмулятор уровня инструкций (instruction-level simulator), разработанный на стадии архитектурного проектирования. Более абстрактная модель, как правило, содержит меньшее количество ошибок, а тот факт, что она разрабатывается независимо, уменьшает вероятность повторения ошибок, допущенных при создании HDL-модели. Данный подход позволяет универсальным образом осуществлять проверку корректности поведения микропроцессора при выполнении различных тестовых программ. Таким образом, отпадает необходимость реализовывать проверки для отдельных тестов. К недостаткам подхода, можно отнести то, что трассы, полученные при помощи упрощенной эталонной модели, могут не отражать все события, которые происходят в HDL-модели (и реальном процессоре). Это приводит к трудностям при сопоставлении трасс.

Список литературы диссертационного исследования кандидат наук Татарников Андрей Дмитриевич, 2017 год

Список литературы

[1] Татарников А.Д. Обзор методов и средств генерации тестовых программ для микропроцессоров. Труды ИСП РАН, т. 29, в. 1, 2017, С. 167-194.

[2] Камкин А.С., Коцыняк А.М., Проценко А.С., Татарников А.Д., Чупилко

М.М.. Генератор тестовых программ для архитектуры ARMv8 на основе инструмента MicroTESK. Труды ИСП РАН, т. 28, в. 6, 2016, С. 87-102.

[3] Татарников А.Д. Построение поведенческих моделей микропроцессоров для генерации тестовых программ. Известия высших учебных заведений. Физика. Том 59. No 8/2. 2016. С. 97-100.

[4] Tatarnikov A. An Approach to Instruction Stream Generation for Functional Verification of Microprocessor Designs. Proceedings of 14th IEEE East-West Design & Test Symposium (EWDTS'2016). 2016. P. 270-273.

[5] Татарников А.Д. Комбинаторная генерация тестовых программ для микропроцессоров на основе формальных спецификаций системы команд. Сборник трудов конференция «Проблемы разработки перспективных микро- и наноэлектронных систем». 2016. Часть II. C. 38-45.

[6] Tatarnikov A. Language for Describing Templates for Test Program Generation for Microprocessors. Proceedings of the Institute for System Programming Volume 28 (Issue 4). 2016. P. 77-98.

[7] Chupilko M., Kamkin A., Kotsynyak A., Protsenko A., Smolov S., Tatarnikov A. Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units. Proceedings of 16th International Workshop on Microprocessor and SOC Test and Verification (MTV 2015), 2015. P. 1-7.

[8] Камкин А.С., Проценко А.С., Татарников А.Д.. Генерация тестовых программ для микропроцессоров на основе спецификаций подсистем памяти. Известия высших учебных заведений. Физика. Том 58. No 11/2. 2015. С. 70-74.

[9] Kamkin A., Protsenko A., Tatarnikov A. An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation

149

Mechanisms. Proceedings of the Institute for System Programming. Volume 27 (Issue 3) 2015. P. 125-138.

[10] Татарников А.Д. Инструмент автоматизации разработки генераторов тестовых программ для микропроцессоров на основе формальных спецификаций. Материалы научно-технической конференции студентов, аспирантов и молодых специалистов НИУ ВШЭ им. Е.В. Арменского. 2015, С. 53-53.

[11] Камкин А.С., Коцыняк А.М., Смолов С.А., Сортов А.А., Татарников А.Д., Чупилко М.М. Средства функциональной верификации микропроцессоров. Труды ИСП РАН, т. 26, в. 1, 2014, С. 149-200.

[12] Камкин А.С., Сергеева Т.И., Смолов С.А., Татарников А.Д., Чупилко М.М. Расширяемая среда генерации тестовых программ для микропроцессоров. Программирование, №1, 2014, С. 3-14.

[13] Kotsynyak A., Tatarnikov A. Generic Knowledgebase for Test Generation. Proceedings of SYRCoSE 2014: 8th Spring/Summer Young Researchers' Colloquium on Software Engineering, 2014. P. 114-117

[14] Kamkin A., Sergeeva T., Tatarnikov A., Utekhin A. MicroTESK: An Extensible Framework for Test Program Generation. Proceedings of SYRCoSE 2013: 7th Spring/Summer Young Researchers' Colloquium on Software Engineering, 2013. P. 51-57.

[15] Kamkin A., Tatarnikov A. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. Proceedings of SYRCoSE 2012: 6th Spring/Summer Young Researchers' Colloquium on Software Engineering, 2012. P. 64-69.

[16] Grant McFarland. Microprocessor Design: A Practical Guide from Design Planning to Manufacturing Professional Engineering. McGraw Hill Professional, 2006, 408 p.

[17] Moore G.E. Cramming More Components onto Integrated Circuits. Electronics Magazine, vol. 86, no. 1, 1965.

[18] Статистика числа транзисторов в микропроцессорах — http://en.wikipedia.org/wiki/Transistor count

[19] Intel® Pentium® 4 Processor. Specification Update, August 2008 (http://download.intel.com/design/intarch/specupdt/24919969.pdf)

[20] Intel® Core™ i7-900 Desktop Processor Extreme Edition Series and Intel® Core™ i7-900 Desktop Processor Series. Specification Update, February 2015. (http://www.mtel .com/content/dam/www/public/us/en/documents/specification-updates/core-i7-900-ee-and-desktop-processor-series-spec-update.pdf)

[21] Beizer B. The Pentium Bug - An Industry Watershed // Testing Techniques Newsletter, TTN Online Edition, September 1995.

[22] Bergeron J. Writing Testbenches: Functional Verification of HDL Models. Kluwer Academic Publishers, 2000. 354 p. doi:10.1007/978-1-4615-0302-6

[23] Bentley B. Validating the Intel® Pentium 4® Microprocessor. Proc. Design Automation Conference (DAC), 2001. pp. 244-248. doi:10.1145/378239.378473

[24] Bentley B. Validating a Modern Microprocessor. Proc. International Conference on Computer Aided Verification (CAV), 2005. pp. 2-4. (http://www.cav2005.inf.ed.ac.uk/bentley CAV 07 08 2005.ppt) (DOI 10.1007/11513988_2)

[25] Matteo Monchiero, Raúl Martínez. Design Cycle for Microprocessors. Intel Corporation, 2011, 34 p.

[26] А.С. Камкин. Верификация микропроцессоров: борьба с ошибками и управление качеством. Электроника: НТБ, №3, 2010. С. 98-104.

[27] Z. Navabi. Languages for Design and Implementation of Hardware. W.-K. Chen (Ed.). The VLSI Handbook. CRC Press, 2007. 2320 p.

[28] S. Mikhani, Z. Navabi. System Level Design Languages. W.-K. Chen (Ed.). The VLSI Handbook. CRC Press, 2007. 2320 p.

[29] P. Mishra, N. Dutt (Eds.). Processor Description Languages. Systems on Silicon. Morgan Kaufmann, 2008. 432 p.

[30] Будылин Ф.К., Полищук И.А., Слесарев М.В., Юрлин С.В. Опыт прототипирования микропроцессоров компании ЗАО «МЦСТ». Журнал «Вопросы Радиоэлектроники», 2012. с. 132.

[31] W.K. Lam. Hardware Design Verification: Simulation and Formal Method-Based Approaches. Prentice Hall, 2005. 624 p.

[32] A. Adir, E. Almog, L. Fournier, E. Marcus, M. Rimon, M. Vinov, A. Ziv. Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification. IEEE Design & Test of Computers, 21(2), 2004. p. 84-93.

[33] Чибисов П.А. Тестирование микропроцессоров и их RTL-моделей приложениями пользователя под OC Linux. Программные продукты и системы, №3, 2012, с. 112-116.

[34] Бобков С.Г., Чибисов П.А. Повышение качества тестирования высокопроизводительных микропроцессоров методами встречного тестирования с анализом функционального тестового покрытия выделенных приложений. Информационные технологии, No8, 2013, с. 26-33.

[35] Хисамбеев И.Ш., Чибисов П.А. Об одном методе построения метрик функционального покрытия в тестировании микропроцессоров. Проблемы разработки перспективных микро- и наноэлектронных систем - 2014. Сборник трудов под общ. ред. академика РАН А.Л. Стемпковского. М.: ИППМ РАН, 2014. Часть II. С. 63-68.

[36] Piziali A. Functional Verification Coverage Measurement and Analysis. New York: Kluwer Academic Publishers. 2004. 216 p.

[37] P. Mishra, N. Dutt. Specification-Driven Directed Test Generation for Validation of Pipelined Processors. ACM Transactions on Design Automation of Electronic Systems, 13(3), 2008. P. 1-36.

[38] E.A. Poe. Introduction to random test generation for processor verification. Technical report. Obsidian Software, 2002, 7 p.

[39] Генератор тестовых программ RISU для тестирования эмулятора QEMU - https://git.linaro.org/people/peter.maydell/risu.git/about/.

[40] Грибков И.В., Захаров А.В., Кольцов П.П. и др. Стохастическое тестирование в системе INTEG. Программные продукты и системы. 2007. № 2. с. 22-26.

[41] Камкин А.С. Генерация тестовых программ для микропроцессоров. Труды ИСП РАН, том 14, часть 2, 2008, с. 23-63.

[42] N. Sharma, B. Dickman, Verifying an ARM Core, EE Times, 2001, 7 p.

[43] А.С. Камкин. Некоторые вопросы автоматизации построения тестовых программ для модулей обработки переходов микропроцессоров. Труды ИСП РАН, 18, 2010. С. 129-149.

[44] Y. Naveh, M. Rimon, I. Jaeger, Y. Katz, M. Vinov, E. Marcus, G. Shurek.

Constraint-Based Random Stimuli Generation for Hardware Verification. AI Magazine, 28(3), 2007. P. 13-30.

[45] P. Mishra and N. Dutt. Specification-Driven Directed Test Generation for Validation of Pipelined Processors. ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 13, Issue 3, 2008, pp. 1-36.

[46] Грибков И.В., Захаров А.В., Кольцов П.П. и др. Развитие системы стохастического тестирования микропроцессоров INTEG. Программные продукты и системы. 2010. № 2. С. 14-23.

[47] MIPS64™ Architecture For Programmers. Volume 1: Introduction to the MIPS64™Architecture. Revision 6.01. MIPS Technologies Inc. 2014. 148 P.

[48] Программный эмулятор VMIPS - http : //www.dgate. org/vmips/.

[49] Сайт компании ARM — http://www.arm.com.

[50] N. Sharma and B. Dickman. Verifying an ARM Core. EE Times. 2001. P 7.

[51] Hrishikesh M.S., Rajagopalan M., Sriram S., Mantri R. System Validation at ARM— Enabling our Partners to Build Better Systems. White Paper. April 2016 (http://www.arm.com/files/pdf/System Validation at ARM Enabling our partners to build better systems.pdf).

[52] Venkatesan D., Nagarajan P. A Case Study of Multiprocessor Bugs Found Using RIS Generators and Memory Usage Techniques. Workshop on Microprocessor Test and Verification, 2014. pp. 4-9. DOI: 10.1109/MTV.2014.28.

[53] Hudson J., Kurucheti G. A Configurable Random Instruction Sequence (RIS) Tool for Memory Coherence in Multi-processor Systems. Workshop on Microprocessor Test and Verification, 2014. pp. 98-101. DOI: 10.1109/MTV.2014.26.

[54] Генератор тестовых программ RAVEN -http://www.slideshare.net/DVClub/introducing-obsidian-software-andravengcs-for-powerpc.

[55] Obsidian Software Inc. "Raven: Product datasheet" 6 P.

[56] R.N. Mahapatra, P. Bhojwani, J. Lee, and Y. Kim. Microprocessor Evaluations for Safety-Critical, Real-Time Applications: Authority for Expenditure No.43 Phase 3 Report. 2009. 43 P.

[57] M. Behm, J. Ludden, Y. Lichtenstein, M. Rimon, M. Vinov. Industrial Experience with Test Generation Languages for Processor Verification. Proceedings of the Design Automation Conference. 2004. pp. 36-40.

[58] M. Aharoni, S. Asaf, L. Fournier, A. Koifman and R. Nagel. FPgen - A Test Generation Framework for Datapath Floating-Point Verification. Proceedings of the Eighth IEEE International Workshop on High-Level Design Validation and Test Workshop (HLDVT'03), 2003. pp. 17-22, ISBN 0-7803-8236-6.

154

[59] M. Aharony, E. Gofman, E. Guralnik, A. Koyfman. Injecting floating-point testing knowledge into test generators. Proceedings of the 7th international Haifa Verification conference on Hardware and Software: Verification and Testing (HVC'11), 2011. pp. 234-241, ISBN 978-3-642-34187-8.

[60] IEEE standard for binary FP arithmetic. An American National Standard, ANSI/IEEEE Std. 754-2008. 58 P.

[61] IBM Floating-Point Test Suite for IEEE 754R Standard -https://www.research.ibm.com/haifa/proiects/verification/fpgen/ieeets.html

[62] Adir A., Fournier L., Katz Y., Koyfman A. DeepTrans - Extending the Modelbased Approach to Functional Verification of Address Translation Mechanisms. High-Level Design Validation and Test Workshop, 2006. pp. 102-110.

[63] Д.Н. Воробьев, А.С. Камкин. Генерация тестовых программ для подсистемы управления памятью микропроцессоров. Труды ИСП РАН, т. 17, 2009, С. 119-132.

[64] Seonghun Jeong, Youngchul Cho, Daeyong Shin, Changyeon Jo, Yenjo Han, Soojung Ryu, Jeongwook Kim, and Bernhard Egger. Random Test Program Generation for Reconfigurable Architectures. Proceedings of 13th International Workshop on Microprocessor Test and Verification (MTV), 2012, 6 p.

[65] T.Li, D.Zhu, Y.Guo, G.Liu, S.Li. MA2TG: A Functional Test Program Generator for Microprocessor Verification. Euromicro Conference on Digital System Design, 2005. pp.176-183.

[66] P. Grun, A. Halambi, A. Khare, V. Ganesh, N. Dutt and A. Nicolau.

EXPRESSION: An ADL for System Level Design Exploration. Technical Report 1998-29, University of California, Irvine, 1998. 26 P.

[67] Инструмент SMV- http://www.cs.cmu.edu/~modelcheck/smv.html

[68] F. Corno, G. Cumani, M. Sonza Reorda, G. Squillero. Efficient Machine-Code Test Program Induction. CEC'2002: Congress on Evolutionary Computation, Honolulu, Hawaii, USA, 2002.

[69] F. Corno et al. Fully Automatic Test Program Generation for Microprocessor Cores. Proc. IEEE Design, Automation and Test in Europe (DATE 03), IEEE CS Press, 2003, pp. 1006-1011.

[70] F. Corno, E. Sanchez, M. Sonza Reorda, G. Squillero. Automatic Test Program Generation - A Case Study. IEEE Design and Test, Special Issue on Functional Verification and Testbench Generation, Volume 21, Issue 2, 2004, pp. 102-109.

[71] Рубанов В.В. Обзор методов описания встраиваемой аппаратуры и построения инструментария кросс-разработки. Труды ИСП РАН, т. 17, 2008, С. 7-40.

[72] M. Freericks. The nML Machine Description Formalism. Technical Report. TU Berlin, FB20, Bericht, 1991/15. 47 p.

[73] M. Hartoog and J. Rowson and P. Reddy and S. Desai and D. Dunlop and E. Harcourt and N. Khullar. Generation of software tools from processor descriptions for hardware/software codesign. In Proceedings of Design Automation Conference (DAC), pages 303-306, 1997.

[74] Страница компании Target Compiler Technologies — http : //www.retarget .com

[75] S. Chandra, R. Moona. Retargetable Functional Simulator using High Level Processor Models. VLSI Design, 2000. P. 424-429.

[76] Страница инструмента GLISS — http://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php37id rubrique=54

[77] H. Cassé, J. Barre, R. Vaillant, P. Sainrat. Fast Instruction-Accurate Simulation with SimNML. Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO), 2011. P. 8-12.

[78] Язык программирования Ruby — http://www.ruby-lang.org

[79] Язык программирования Python — https://www.python.org

[80] Язык программирования Perl — https://www.perl.org

[81] Flanagan D., Matsumoto Y. The Ruby Programming Language. O'Reilly Media, Sebastopol, 2008, 446 p.

[82] Среда генерации тестовых программ для микропроцессоров — http: //forge.ispras .ru/proi ects/microtesk

[83] Язык программирования Java — https://en.wikipedia.org/wiki/Java (programming language)

[84] Библиотека Fortress — http://forge.ispras.ru/proiects/solver-api

[85] Cok D.R. The SMT-LIBv2 Language and Tools: A Tutorial. GrammaTech, Inc., Version 1.1, 2011.

[86] Дроздов А.Ю., Новиков С.В. Эффективный алгоритм построения формы статического единственного присваивания. Информационные технологии, № 3, 2005.

[87] Ахо А., Лам М., Сети Р., Ульман Д. Компиляторы: принципы, технологии и инструментарий. 2 изд. Вильямс, 2008.

[88] Steven S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997, 887 p.

[89] Инструмент ANTLR - http://www.antlr.org/

[90] Terence Parr. The Definitive ANTLR Reference: Building Domain-Specific Languages. The Pragmatic Bookshelf, 2007, 384 p.

[91] Terence Parr. Language Implementation Patterns: Create Your Own Domain-Specific and General Programming Languages. The Pragmatic Bookshelf, 2009, 350 p.

[92] Библиотека StringTemplate - http://www.stringtemplate.org/

[93] Библиотека Java SoftFloat - http://forge.ispras.ru/proiects/jsoftfloat

[94] Библиотека Berkeley SoftFloat -

http: //www.i hauser. us/arithmetic/SoftFloat.html

[95] Интерпретатор JRuby - http://jruby.org/

157

[96] База знания TestBase - http://forge.ispras.ru/proiects/testbase

[97] L. Moura and N. Bjorner. Z3: An Efficient SMT Solver. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008, pp. 337-340.

[98] Решатель ограничений CVC4 - http://cvc4.cs.nyu.edu

[99] Камкин А.С. Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций. Диссертация на соискание ученой степени кандидата физико-математических наук. Москва, 2009.

[100] Микропроцессоры НИИСИ РАН - https://www.niisi.ru/devel.htm

[101] Сайт компании Imagination Technologies - https://www.imgtec.com/

[102] Дмитрий Мякин. Армейский компьютер «Восход» на архитектуре КОМДИВ64 готов к экстремальным условиям, 2016 (https://3dnews.ru/939502).

[103] MIPS64™ Architecture For Programmers. Volume 2: The MIPS64™ Instruction Set Reference Manual. Revision 6.04. MIPS Technologies Inc. 2015. 551 P.

[104] MIPS64™ Architecture For Programmers. Volume 3: MIPS64™/microMIPS64™ Privileged Resource Architecture. Revision 6.03. MIPS Technologies Inc. 2015. 368 P.

[105] Сайт ARM - http: //www.arm.com

[106] Mallya H. The Backstory of How ARM Reached a Milestone of 86 Billion Chips in 25 Years. July 19, 2016 (https://yourstory.com/2016/07/arm-holdings-story/)

[107] Morgan T.P. ARM Holdings Eager for PC and Server Expansion. Record 2010, Looking for Intel Killer 2020. February 1, 2011 (http://www.theregister.co.uk/2011/02/01/arm holdings q4 2010 numbers/).

[108] Sims G. Custom Cores versus ARM Cores, What Is It All About? January 7, 2016 (http://www.androidauthority.com/arm-cortex-core-custom-core-kryo-explained-664777/).

[109] ARM Architecture Reference Manual. ARM DDI 0487A.f, ARM Corporation,

2015. 5886 P.

[110] Программный эмулятор QEMU- http://www.qemu.org/

[111] Программный эмулятор для ARMv8 на основе QEMU -https://forge.ispras.ru/proiects/qemu-armv8

[112] Архитектура PowerPC - https://en.wikipedia.org/wiki/PowerPC

[113] Wetzel/Poughkeepsie/IBM. "PowerPC User Instruction Set Architecture". Book I. Version 2.02, 28 January 2005. 230 P.

[114] Wetzel/Poughkeepsie/IBM. "PowerPC Virtual Environment Architecture". Book II. Version 2.02, 28 January 2005. 68 P.

[115] Wetzel/Poughkeepsie/IBM. "PowerPC Operating Environment Architecture". Book III. Version 2.02, 28 January 2005. 135 P.

[116] Архитектура RISC-V - https://en.wikipedia.org/wiki/RISC-V

[117] Сайт RISC-V Foundation - https://riscv.org

[118] Michael Larabel. NVIDIA Is Building Its Next-Gen Falcon Controller Using RISC-V. 26 July 2016.

(https://www.phoronix.com/scan.php?page=news item&px=NVIDIA-RISC-V-Next-Gen-Falcon)

[119] David Manners. Samsung Defection From ARM to RISC-V. 28 November

2016. (https://www.electronicsweekly.com/blogs/mannerisms/dilemmas/samsung-defection-arm-risc-v-2016-11)

[120] Микропроцессор PULPino (основан на RISC-V) - http://www.pulp-platform.org

[121] Andrew Waterman, Krste Asanovic. The RISC-V Instruction Set Manual. Volume I: User-Level ISA. Version 2.2. University of California, Berkeley. May 7, 2017. 145 P.

[122] Andrew Waterman, Krste Asanovic. The RISC-V Instruction Set Manual. Volume II: Privileged Architecture. Version 1.10. University of California, Berkeley. May 7, 2017. 91 P.

Приложения

«Утверждаю»^??

^ 'г,«1»""" ^

Зам. директора г^^н^нОэлектрогшус Федерального госудажгренноге учреждения "Федеральный натаф^/ центр Шучно*» исследовательский рнстйтут . ]• системных: исследований Российской академии наук"'.й

_^ у*_

« 20 » июля 17 года

акт

о внедрении результатов диссертационной работы Татарникова Андрея Дмитриевича

Комиссия в составе: председатель:

зав. отделением разработки вычислительных систем к.т.н. Аряшев Сергей Иванович, члены комиссии:

зав. сектором отдела архитектур высокопроизводительных микропроцессоров к.т.н. Корниленко Александр Владимирович, зав. отделом сопровождения разработок Сидоров Сергей Александрович, зав. группой отдела тестирования микросхем Слинкин Дмитрий Игоревич, составила настоящий акт о том, что разработанный в диссертационной работе Татарникова А.Д. метод автоматизации конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций и реализующий его инструмент МюгоТЕБК использованы при выполнении ОКР «Процессор-5» и «Процессор-6» по созданию микропроцессоров 1890ВМ8Я и 1890ВМ9Я в ФГУ ФНЦ НИИСИ РАН.

Использование указанных результатов диссертации позволяет повысить эффективность тестирования микропроцессоров и их моделей, сократить время, требующееся на проведение работ по функциональной верификации моделей проектируемых микропроцессоров. Использование генератора тестовых программ, разработанного при помощи инструмента МлсгоТЕБК, позволило выявить несколько серьезных ошибок в подсистеме управления памятью и в буфере трансляции адресов в ИТЬ-модели микропроцессора 1890ВМ8Я.

Председатель комиссии: Члены комиссии: зав. сектором к.т.н. зав. отделом зав. группой