В главе 3 мы определим последовательную DLX машину в духе [PH94] и докажем, что она работает. Доказательства, главным образом, бухгалтерские. Мы должны выполнить упражнения, потому что позже мы докажем правильность конвейерных машин, показав, что они моделируют последовательные машины, чья правильность уже установлена.
В разделе 4 мы имеем дело с конвейеризацией, отсроченным переходом, пересылкой результата и аппаратной взаимной блокировкой. Мы покажем что механизм отсроченного перехода может быть заменен механизмом, называемым нами "задержанный PC (delayed PC)", который задерживает все выборки команд, не выполняя переходов.3. Мы разделим машины на пути данных, управляющий автомат, механизм пересылки и механизм останова. Конвейерные машины получены из подготовленных машин, упомянутых выше почти прямым преобразованием.
Глава 5 имеет дело с темой, которая хитро рассматривается и не часто встречается в литературе: прерываниями. Даже определение, чем должен заниматься механизм прерываний, оказывается не настолько просто. Причина в том, что прерывание - своего рода вызов процедуры; вызовы процедуры в свою очередь - концепция языка высокого уровня, на уровне абстракции этот путь выше уровня аппаратных спецификаций.
Достигнутая точность, оказывается, не столь плоха. После того, как все понято для последовательных машин, мы генерируем конвейерную машину путем преобразования подготовленных последовательных машин. Но взаимодействие аппаратных средств прерываний и схем пересылки непростое, в особенности, когда это касается пересылки регистров специального назначения подобных, например, регистру, который содержит маски прерываний.
3У нас гораздо более удобные доказательства, так как они были проверены в PVS.
Глава 6 имеет дело с кэшэм. В частности, мы определим шинный протокол, в соответствии с которым происходит обмен данными между CPU, кэшэм и основной памятью, и определим автоматы, которые реализуют этот протокол. Мы объясним автоматы, но мы не будем доказывать, что они реализуют протокол. Модель проверки [HQR98] намного лучше подходит для проверки выражений этого вида.
Глава 7 вообще не содержит никаких конструкций. Только стандарт IEEE с плавающей запятой перефразирован на математическом языке и доказаны теоремы об округлении. Вся глава - теория. Это - инвестиции в главу 8, где мы проектируем полностью IEEE-совместимые сопроцессоры для операций с плавающей точкой с denormals и исключениями, сумматором двойной точности, множителем, итерационным делением, преобразованием форматов, округлением. И все это только на 120 страницах ;-) .
В главе 9 мы интегрируем конвейерный сопроцессор для операций с плавающей точкой в DLX машину. Как можно было ожидать, управление становится более сложным: и потому, что команды имеют переменное время ожидания и потому, что итерационное деление не полностью конвейеризировано. Мы вкладываем много усилия в очень удобный механизм пересылки. В частности, этот механизм позволит ускориться режиму округления операций с плавающей запятой. Это, в свою очередь, разрешает интервальной арифметике быть реализованной при поддержке конвейерных операций машины.
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.