Моделирование арифметико-логического устройства для вычитания УДЦ
Федеральное
государственное бюджетное образовательное учреждение
высшего
профессионального образования
ИВАНОВСКИЙ
ГОСУДАРСТВЕННЫЙ ЭНЕРГЕТИЧЕСКИЙ УНИВЕРСИТЕТ
ИМЕНИ
В. И. ЛЕНИНА
Кафедра
программного обеспечения компьютерных систем
Курсовая
работа
по
дисциплине:
“Теория
вычислительных процессов”.
Тема:
«Моделирование АЛУ для вычитания УДЦ»
Выполнил:
студент гр. 3-42
Михальков Г.М.
Иваново
Оглавление
Введение
Анализ
Алгоритм
Семантика
Линейная
схема
Верификация
Сети
петри
Вывод
Введение
1) Моделирование АЛУ для вычитания УДЦ для
18 разрядов (программа должна показывать преобразования и вычисления, и
правильно выполнять заданные операции);
) Написать аксиоматическую семантику
команды ассемблера.
Анализ
Операция сложения выполняется в арифметико-логическом
устройстве - АЛУ (см. рис.1).
рис.1 Структурная схема АЛУ для вычитания
На рис.1 представлена структурная схема АЛУ для
вычитания 18-разрядных целых чисел. В состав АЛУ входят: входной регистр
первого слагаемого RA,
входной регистр слагаемого RB;
стек сумматора ST;
сумматор “--” (в данной реализации - арифметический сопроцессор 8087, отсюда
вытекает нестандартная архитектура сумматора) для нахождения разности; выходной
регистр сумматора совмещен со входным регистром RA.
По входной шине в регистр А (RA) и в регистр В
(RB) заносятся операнды, представленные УДЦ формате. Далее, происходит
нахождение разности операндов. Результат операции записывается во входной
регистр RA, стирая
предыдущее содержимое.
Алгоритм нахождения разности УДЦ можно разбить
на следующие этапы:
· занесение чисел RA
и
RB
· преобразование их во внутреннее
представление сумматора
· вычисление разности
· преобразование результата к УДЦ
· перезапись RA
Алгоритм
Блок - схема подпрограммы сложения чисел
Семантика
Операционная семантика команды rol al, 1
L1(al)
L1(al)
. q01S1
Top1
q02
. q02S2Top2q11
. q11S1
L1 q21
. q21X1
B1 q31 (®)St1
. q31X1
L1 q12
. q12X2B2q22(¬)St1
. q22X2
L2 q21
. q21#1
B1 q41
. q41X1
Top1 q51
. q51X1
B1 q32
(®)St1
. q32X2B2q42(¬)St1
. q42X2Top2q52
. q52X2
B2 q62
(®)St1
. q62X2
L2 q61
. q61X1B1q71(¬)St1
. q71X1
L1 q42
Операционная семантика команды shl
al, 1
L1 (al):
1. q01S1Top1q11
2. q11X1L2q21
3. q21X1B1q31(
)St1
4. q31X1R1q41
5. q41X1(
)St1 q51
6. q51X1L1q11
7. q21#1R1q61
8. q61S101q71
9. q71S1Top1q81
Линейная схема
1. НАЧАЛО на 3
. ПРИСВОИТЬ si,
строка
3. ПРИСВОИТЬ cx, 0
. ЕСЛИ ([si]
< 30h) ТО на 9
. ЕСЛИ ([si]
> 39h) ТО на 9
. УВЕЛИЧИТЬ si
. УВЕЛИЧИТЬ cx
. на 4
. ВЕРНУТЬ cx
10. КОНЕЦ
Символы:
· cx
- переменная, количество символов в строке
· si
- указатель на символ строки, [si]
- символ строки
· НАЧАЛО, КОНЕЦ - специальные
символы
Операторы:
· условные операторы (ЕСЛИ … ТО …
ИНАЧЕ …)
· операторы перехода (на)
· операторы присвоения (ПРИСВОИТЬ
операнд 1, операнд 2)
· операторы возврата (ВЕРНУТЬ операнд)
Функции:
· Вывод() - вывести строку;
Верификация
Без ветвления:
ra = r1
rb = r2
sm = ra
- rb
(r1
>= r2) { ra
= r1; rb
= r2; sm
= ra - rb
} sm <= ra
(r1
>= r2) { ra
= r1; rb
= r2; } ra
- rb <= ra
(r1
>= r2) { ra
= r1 } ra
- r2 <= ra
(r1
>= r2) è
r1 - r2
<= r1
true & true è
trueè true
ветвлением:
(last==1)
{ra=r1;}
{ra=0;}
) ((last=1)˅(last=0))&(last=1){ra=r1}(ra=r1)˅(ra=0);
((last=1)˅(last=0))&(last=1)
→ (r1=r1)˅(r1=0);& true → true → true .
) ((last=1)˅(last=0))&¬(last=1){ra=0}(ra=r1)˅(ra=0);
((last=1)˅(last=0))&¬(last=1)
→ (0=r1)˅(0=0);& true → true → true .
Верификация цикла:=count;
{(…);
} while (i>0);
= ((countÎN)˅(count=0));=
(i>0);= (i=i-1);= (i ≤ 0).
((countÎN)˅(count=0))&(i≤count){while
i>0 do i=i-1 end}i ≤ 0;
1. Инвариант цикла удовлетворяется при
входе в цикл:
((countÎN)˅(count=0))
→ (i≤count)˅ false → true→ true
2. Инвариант цикла удовлетворяется при
проверке условия выполнения цикла:
(i≤count){
(i>0)} (i≤count)
true → true
3. Инвариант цикла удовлетворяется в теле
цикла:
(i≤count)
& (i>0) {i=i-1} (i≤count)
(i≤count)
& (i>0) → (i-1≤count)
(i≤count)
& (i>0) → (i≤count+1)& true → true → true
4. Инвариант цикла и отрицание условия
выполнения имплицируют постусловие:
(i≤count)
&¬ (i>0) → (i ≤ 0)
(i≤count)
& (i ≤ 0)→ (i ≤ 0)& true → true → true
Сети Петри
устройство
вычитание семантика верификация программа
Вывод
В данной работе была написана программа
моделирования АЛУ для вычитания УДЦ. Также была проведена верификация линейного
участка программы, участка, содержащего ветвления, цикла, была описана
операционная семантика и построены сети Петри для подпрограммы.