Формальная верификация процессора с устройствами поддержки виртуальной памяти

• Автор: Далингер, Яков
• Шифр специальности: 05.00.00
• Научная степень: Кандидатская
• Год защиты: 2006
• Место защиты: Саарбрюккен
• Количество страниц: 152 с. : ил.

День коллоквиума: 9 Июня 2006

Декан Prof. Dr.-Ing. Thorsten Herfet Председатель комиссии: Prof. Dr.-Ing. Gerhard Weikum

1. Член комиссии: Prof. Dr. Wolfgang J

2. Член комиссии: Prof. Dr. Peter-Michael Seidel научный сотрудник: Dr. Mark Hillebrand
Нижесказанным я подтверждаю, что представленная работа была выполнена без помощи третьего лица и без использования других вспомогательных материалов. Все данные используемые не на прямую или концепции взятые из других источников помечены ссылками. Данная работа в этой или подобной форме до настоящего времени не была представлена в качестве диссертации в комиссии по аттестации ни в Германии, ни за рубежом.

Саарбрюккен, Июнь 2006

Слова благодарности

Я благодарен моей жене Юлии и моим родителям за оказанную поддержку в течении лет когда данная работа выполнялась и описывалась.

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

Я также благодарю сотрудников кафедры проф. Пауля, в особенности Марка Хилдебранда и Свена Байера, за многие инициирующие дискуссии

Краткая аннотация
В данной работе будет представлена формальная верификация блока поддержки виртуальной памяти который требует специальных условий для работы. Также будет представлено формальное доказательство сложного процессора VAMP с поддержкой трансляции адреса при помощи блока поддержки виртуальной памяти. VAMP процессор является 32 битным RISC процессором исполняющим команды не в последовательности их поступления на исполнение с набором инструкций DLX, имеет модуль для вычислений с плавающей запятой согласно IEEE стандарта и блок доступа к памяти. VAMP также поддерживает точные прерывания, как внутренние так и внешние. Процессор смоделирован на уровне логических элементов и доказан по отношению к своей спецификации. Объект исследований в данной работе базируется на уже имеющимся формальном доказательстве процессора VAMP без поддержки трансляции адреса [Веу05] и на ранее разработанных неформальных спецификации, имплементации и доказательства корректности блока поддержки виртуальной памяти [НІІ05].

Определение 2.1.7 Определим предикат гз_гед_ргос, как предикат запроса процессора следующим образом:
гз_гед_ргос(1, С, Ьгс) :=
(£ > О =Ф- ~|£гс(£ — 1 ).Ъизур) Л (£ < б) Л £гс(£).гедр Л Ьгс{).Ъизур Л /£" € [£ : £;[ : Ьгс(Ь").Ьизур
Сигнал Ъизур должен быть активирован в течении всего запроса процессора за исключением последнего цикла. Поскольку изменение состояний входов гприЬвр может происходить только когда Ьизур неактивен (Определение 2.1.6) можно доказать с помощью индукции следующую лемму, которая гласит, что в течении запроса процессора состояние всех входов процессора не изменяются.
Лемма 2.1.8 Состояние всех входов процессора стабильны в течении запроса процессора:
е N Л < £ < ?
(гз_геу_ргос{Ь) С, £гс) Л р_ге_гд_.5£аЫе(£гс)) =>-Ьгслпрвр — Ьгс(С) лпрЫвр
Доказательство: Пусть £ < С < £/;. Докажем данное утверждение с
помощью индукции по £'. Для базы индукции £ = £' все очевидно и ничего доказывать не надо. Для индукционного шага б —> £' + 1 у нас есть, что
£' < £" Л
га_гед_ргос(£, Д, £гс) Л р_гед_га__з£аМе(£гс) Л
ЛприЬЗр = №с(1:') лпрЫвр