Детальный проект конвейерного RISC процессора (Глава 5 "Обработка прерываний"), страница 26

Таблица 5.16 Назначение событий внешних прерываний, когда объединяются две последовательности команд Pи Q

Доказательства, работающие с допустимостью ISR (раздел 5.4) рассуждают только о сигнале JISRи значениях регистров и памяти, видимых программисту на ассемблере, т.е., файлах регистров общего и специального назначения, двух PC и двух памятях IM и DM:

C = {GPR[0],...GPR[31], SPR[0],..., SPR[5], PC', DPC, DM, IM}.

Поэтому для моделирования сигнал JISRи содержание хранилища Cимеет повышенный интерес.

Пусть P = I₀ ,..., I_p ,..., I_p+δ и P' = I₀ ,..., I_p – две последовательности команд расширенные последовательностью внешних событий, как определено выше. Последовательность P выполняется конвейерной конструкцией DLX_П а P' последовательной конструкцией DLX_∑. Пусть команда I₀ предшествует JISR

JISR_∑^-1 = 1    и JISR_П⁰ = 1,

и пусть обе конструкции стартуют в одинаковой конфигурации, т.е.,

VR € CR_∑⁰ = R¹_П .

Пусть T_p и T_p' означают циклы, в которых I_p обрабатывается на этапе обратной записи

I_П(4, T_p) = I_∑(4, T_p') = p /\ ue.4_П^Tp = 1.

Тогда проинициализированные PC имеют значения PC'_∑⁰ = SISR + 4 и DPC_∑⁰ = SISR. Для любой команды I_i € P', любого этапа k, и любых двух циклов T, T ' при

I_П(k,T)=I_∑(k, T ') = i /\  ue.k_П^T = 1

должны выполняться следующие два требования:

Рисунок 5.20 Пары (k, T) конвейерного выполнения. Поле 0 покрывается по гипотезе моделирующей теоремы, поля 1 и 2 соответствуют требованиям 1 и 2.

1.    (a) для всех сигналов S этапа k, которые являются входами регистра R€ out(k) обновляемого в конце циклаT:

S_П^T = S_∑^{T '},

(b) для всех регистров R € out(k), которые видимы или обновляются в конце цикла T:

(c) для любой ячейки M памяти данных DM и k = 3:

m_п^t+1 = m_∑^{t '+1} = m_i,

2. и для любых R € C и T = T_p

R_П^T+1 = R_∑^{T '+1} = R_p .

Что касается конвейерного выполнения, существует три типа пар (k, T) для которых значения S^Tи R^T+1сигналов Sи выходных регистров Rэтапа kпредставляют интерес (рисунок 5.20):

• Для первого цикла теорема делает предположение о содержимом всех регистров и памяти R € Cнезависимо от этапа, которому они принадлежат (поле 0).

• Требование 1 покрывает все пары (k, T), для которых I_П(k, T) определен и лежит между 0 и p(поле 1).