|
Требование 2 – новое, и поэтому требует полного доказательства. Для выходных регистров этапа 4 требование 1 уже подразумевает требование 2. Кроме того, в конструкциях DLX∑и DLXПпамять команд никогда не обновляется. Таким образом, требование 2 должно быть доказано только для двух программных счетчиков PC' и DPC, и для памяти данных DM. Последовательность команд P' последовательной конструкции создавалась так, что команда Ipвызывает прерывание. Так как сигнал JISRгенерируется на этапе 4, требование 1 подразумевает JISR∑T ' p = JISRПTp= 1. В каждой конструкции оба PC инициализируются при активном сигнале JISR, и следовательно DPC∑T ' p + 1 = SISR = DPCПTp + 1 PC'∑T ' p + 1 = SISR+ 4 = PC'ПTp+1. Память данных DM принадлежит набору out(3). Для этапа 3 обе функции планирования подразумевают IП(3, Tp - 1) = I∑(3, T 'p - 1) = p. |
dpcП0 = DPCП1 = DPC∑0 = DPCΣ1.
В последовательной конструкции память данных обновляется только когда команда на этапе 3, т.е., когда full.3 = 1. Тогда требование 1 подразумевает, что
|
|
JISR сигнализирует только если full.4 = 1. Для цикла Tp' последовательный механизм останова тогда подразумевает, что
Таким образом, память данных не обновляется в течении JISR, и следовательно
DM∑T 'p = DM∑T ' p + 1
В конвейерной конструкции сигнал разрешения записи памяти данных генерируется как
Dmw.3 = Dmw'.3 /\ full.3 /\ (JISR NOR reset).
Так как сигнал Dmw.3 блокируется при активном сигнале JISR, память данных не изменяется в течении цикла Tp , и следовательно,
|
Этим завершается доказательство требования 2.
|
Теперь мы рассмотрим произвольную последовательность команд Q, которая обрабатывается конвейерной конструкцией DLX, и которая прерывается несколькими прерываниями типа non-aborting. Такая последовательность Qможет быть разломана на несколько непрерывных подпоследовательностей pi = I(i, 0) ,..., I(i, p1) ,..., I(i, pi + δi) . |
Это значит, что для любой последовательности Pi , команда I(i, 0) предшествующая JISR, I(i, pi)является только командой Pi которая вызывает прерывание, и команда I(i, pi + δ1) является последней командой выбранной перед переходом на ISR. Для последовательного выполнения мы рассмотрим последовательность команд Q' = P1',P2' ,... которая происходит из последовательности Qвыбросом команд вызывающих JISR, т.е.,
События внешних прерываний назначены, как и прежде. Функции планирования расширенны очевидным способом. Для конструкций DLX∑и DLXП,
I∑(k, T) = (i, j) и IП(k,T) = (i, j)
Означает, что в цикле Tконвейерного этапа kвыполняется команда I(i, j).
Подобно обеим конструкциям DLX без аппаратуры прерываний, конструкции DLX∑ и DLXПстартуют сбросом, а не JISR. Леммы 5.8 и 5.10 подразумевают, что после сброса обе конструкции изящно пойдут вверх; один цикл после сброса JISR = 1 и конструкции инициируют переход на ISR(0). Таким образом, теперь мы можем сформулировать общую моделирующую теорему для конструкций DLX∑и DLXП:
|
Теорема 5.12 |
Пусть Q = P1 , P2 ,.... и Q' = P'1 , P2 ,... – две последовательности команд расширенные последовательностью внешних событий, как определено выше. Последовательность Q выполняется конвейерной конструкцией DLXП а Q' - последовательной конструкцией DLX∑. При последовательном выполнении сброс дается в цикле - 2, в то время как при конвейерном выполнении, сброс дается в цикле - 1 :
reset∑-2 = 1 = resetП-1.
Пусть обе конструкции стартуют с одинаковым содержанием, т.е., любой регистр и памятьR путей данных удовлетворяет
RΣ-1 = RП0, (5.4) и пусть первая команда I(1, 0) предшествует JISR
JISR∑-1 = 1 = JlSSП0.
Для каждой пары (Pi , P'i ) подпоследовательностей, конструкция DLXП выполняя Pi моделирует конструкцию DLX∑ на P'i в значении теоремы 5.11.
|
ДОКАЗАТЕЛЬСТВО |
Как показано в доказательстве требования 2 теоремы 5.11, обе конструкции инициализируют PC при JISR одинаково, таким образом
(PC', DPC)∑0 = (PC', DPC)1П.
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.
