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

• Автор: Негода, Дмитрий Викторович
• Шифр специальности: 05.13.12
• Научная степень: Кандидатская
• Год защиты: 2005
• Место защиты: Ульяновск
• Количество страниц: 157 с. : ил.

Оглавление
Введение.

1. Анализ технологий проектирования симуляторов

1.1. Модели микропроцессоров.

1.2. Классификация симуляторов.

1.3. Базовые технологии проектирования симуляторов.

1.4. Оптимизация симуляторов по быстродействию.

1.5. Выводы по первой главе

2. Исследование методов оптимизации симуляторов по быстродействию .

2.1. Методы анализа и трансформации программ.

2.1.1. Алгебра языков программирования

2.1.2. Синтаксис и семантика языка Vi
2.1.3.Реляционная хоаровская логика.
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.3. Отложенное вычисление флагов
2.3.1. Функциональная модель
2.3.2. Эксперимент
2.3.3. Автоматизация оптимизирующего преобразования.
2.4. Выводы по второй главе.
3. Автоматизация тестирования симуляторов
3.1. Автоматизация тестирования программ
3.2. Существующие методы тестирования симуляторов
3.3. Метод тестирования симуляторов на основе генерации тестов и использования прототипа.
3.4. Выводы по третьей главе.
4. Автоматизация проектирования симуляторов микроконтроллеров и интерация моделей микропроцессорных устройств в систему
4.1. С труктура МПС
4.2. Взаимодействие компонентов МПС
4.3. Маршрутизатор сообщений.
4.4. Планирование и дельтазадержка
4.5. Дизассемблер
4.6. Визуальная среда симуляции МПС
4.7. Симулятор микропроцессора 6. Создание новых симуляторов и моделей.
4.8. Выводы по четвертой главе.
Заключение. . .
Список используемых сокращений
Публикации по теме диссертации
Литература


Показывается, что наряду с традиционно используемыми средствами оптимизации, встроенными в компиляторы, существенный эффект дают оптимизирующие преобразования исходных кодов. В третьей главе предлагается и исследуется метод тестирования симуляторов, отличающийся от известных тем, что использует исходный код симулятора для генерации тестов машинных команд, которые затем выполняются на существующих интерпретаторах машинных команд - либо реальных микропроцессорах, либо заведомо правильных симуляторах. Благодаря этому существенно сокращаются трудозатраты на тестирование симуляторов. В четвертой главе проводятся экспериментальные исследования, направленные на создание средств интеграции симуляторов в САПР МПС. Излагаются результаты разработки архитектурного каркаса и его применение для создания экспериментальной САПР МПС на базе МП 6. Автор выражает благодарность своему научному руководителю, д. ВТ УлГТУ Соснину П. И., а также 1руп-пе исследователей лаборатории АОС и участникам постоянно действующего городского семинара «Встроенные системы и коммуникации», где автор неоднократно докладывал результаты своих исследований. В системах автоматизированного проектирования микропроцессорных систем (САПР МПС) часто оперируют не реальным микропроцессорным устройством, а некоторой математической моделью, которая абстрагирует реальную МПС, моделируя лишь некоторые интересующие разработчика свойства. В данной диссертации мы ограничиваемся только функционально-логическими моделями, игнорируя физический или информационный аспекты МПС. В зависимости от цели исследования, применяются различные функционально-логические модели. Мура [] и другие. Вторая группа моделей специфицирует операцію]тую семантику МП. К этой группе относятся следующие модели: абстрактные машины состояний Юрия Гуревича (Abstract State Machines), системы перезаписи термов, алгоритмические модели. Симулятор МП включает его алгоритмическую модель и решает над ней некоторую задачу сішуляции - например, задачи оценочного моделирования, отладки, виртуализации и т. Одной из важнейших задач в области моделирования МПС является верификация моделей, или, более формально, является ли одна автоматная модель (например, программа на VHDL) реализацией другой автоматной модели (например, спецификации системы команд). Существует два подхода к верификации проектных решений МПС: формальные доказательства и симуляция. Мура [] и логики высшего порядка []. Обе спецификации (например, системы команд МП и се аппаратной реализации) записываются в терминах используемой логической оболочке, после чего используется формальный вывод для доказательства теорем о гомоморфизме одной модели в другую (обычно используется автоматический вывод). Формальная спецификация корректности МП и МПС может длиться месяцы и даже годы. При использовании симуляции верификация заключается в генерации тестовых последовательностей, прогоне тестовых данных на некоторой отлаженной алгоритмической модели (т. На практике симуляция является более удобной и наиболее распространенной альтернативой формальным доказательствам или использованию дорогостоящих аппаратных стендов при отладке МПС. Идея симуляции сформулирована еще Тьюрингом в []: одна универсальная машина Тьюринга (инструментальная машина) может имитировать поведение другой, целевой машины. Вычислительный процесс можно разбить на последовательные дискретные моменты времени. В каждый момент времени состояние вычислителя определяет значение состояния в следующем моменте времени. Эту идею можно формализовать, если рассматривать функцию перехода состояния / :А-> А и дискретное время Т = {0,1,. T,a€A. Таким образом, Г(Ца) означает состояние, которое примет система через ( шагов времени (итеративная функция, []). Природа множеств А и Т зависит от уровня абстракции, на котором моделируется система. Ш генератор. Для моделирования времени полезно рассматривать также темпоральную алгебру (Г|0,Г + 1), в которой присутствует функция получения каждого последующего временного интервала. Потоком (stream) se[7’-> Л] называют функцию от времени, порож-* дающую бесконечную последовательность единиц данных. ТхА —!