В этой книге мы используем математический формализм точно таким же способом. Это - основная причина, по которой мы можем охватить быстро так много материала.
• Мы уже заявляли это выше: читатель, по крайней мере, может использовать доказательства правильности из этой книги как высокоструктурированные и формализованные объяснения относительно того, как, по мнению авторов, работают конструкции.
• Но это еще не все. В течение последних лет множество усилий было вложено в развитие компьютерных систем, которые позволяют формулировать теоремы и доказательства таким образом, что доказательства фактически могут быть проверены компьютером. К настоящему времени доказательства, подобные приведенным в этой книге, могут быть с разумными усилиями введены в автоматизированные системы доказательств.
Действительно, во время написания (февраль 2000) правильность машины, близко связанной с машиной из главы 4 (со слегка различным основным механизмом ускорения), была проверена с использованием системы PVS [CRSS94, KPM00]. Также была проведена проверка всех конструкций из главы 2, используемых в главе 4. Производится и прогрессирует гладко (пока) проверка большинства частей книги, включая сопроцессор для операций с плавающей точкой из главы 8.
Ключевые концепции
Есть три ключевых концепции, которые позволили нам разработать материал для этой книга очень быстро и в то же время точно.
1. Мы делаем строгое различие между числами и их представлением. Простой формализм этого получен в главе 2. Это сразу же помогает уменьшить доказательства правильности многих вспомогательных схем для облегчения упражнений. Более важно то, что этот формализм поддерживает порядок - и здравомыслие читателя - в конструкции сопроцессоров для операций с плавающей точкой, которые, случается, оперируют числами в 7 различных форматах.2
2. Детали конвейеризации очень хитрые. Как инструмент к их лучшему пониманию, мы представим в главе 4 подготовленные последовательные машины. Это машины, которые имеют путь данных конвейерной машины, но работают последовательно. Они очень просты для понимания.
Конвейерные машины должны моделировать подготовленные последовательные машины в довольно прямом формальном смысле. Таким образом, мы можем, по крайней мере,
2упакованные одиночной и двойной точности, распакованные одиночной и двойной точности, двоичные числа, двоичные дополнительные числа и смещенные целые числа
легко сформулировать то, что конвейерные машины, как предполагается, делают. Показывая, что они действительно делают то, что от них требуется, иногда будем включать некоторые короткие, но тонкие аргументы о планировании команд в конвейерах.
3. В главе 7 мы опишем алгебру основанную на [EP97]. Это разрешит нам формулировать очень краткие утверждения о поведении схем с плавающей запятой. Это позволит нам разработать полностью структурным способом схемотехнику сопроцессора для операций с плавающей точкой.
Выделения
Мы заканчиваем введение, выделяя некоторые результаты из глав этой книги. В главе 2 мы разработаем множество вспомогательных схем для дальнейшего использования: различные счетчики, сдвигающие устройства, декодеры, сумматоры, включая сумматоры предвидения переноса и множительные устройства с Booth recoding. В большой степени мы определим управление машинами в соответствии с диаграммами конечных состояний. Опишем простой перевод этих диаграмм состояний в аппаратные средства.
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.