1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
\section{Instruction Set}
\label{sec:instr}
\subsection{The Instruction Cycle}
The instruction cycle is a function $\State\to\State$. It is defined as
follows:
$$\mathit{cycle}(\prog,\mem) \eqdef (\prog, \instr{\mem.\pc}{\prog,\mem})$$
Here, $\instrop$ is a function that maps words to instructions: $\instrop :
\Word4 \to \Mem \to \Mem$. It is defined in \autoref{sec:instr}.
\subsection{Instructions}
The binary representations of the commands defined can be found in
\autoref{fig:instr:instr-set}.
\begin{table}[h]
\centering
{\tt
\begin{tabular}{!>{\normalfont}l | ^l | *{4}{|^c}}
\rowstyle{\normalfont\bfseries}
Instruction name & Assembly & 3 & 2 & 1 & 0 \\\hline
Addition & add & 0 & 0 & 0 & 0 \\\hline
Subtraction & sub & 0 & 0 & 0 & 1 \\\hline
Rotate left & rol & 0 & 0 & 1 & 0 \\\hline
Shift left & shl & 0 & 0 & 1 & 1 \\\hline
Logical AND & and & 0 & 1 & 0 & 0 \\\hline
Logical OR & or & 0 & 1 & 0 & 1 \\\hline
Logical XOR & xor & 0 & 1 & 1 & 0 \\\hline
Logical NOT & not & 0 & 1 & 1 & 1 \\\hline
Store register & str & 1 & 1 & 0 & 0 \\\hline
Load register & ld & 1 & 1 & 0 & 1 \\\hline
Conditional jump & cjmp & 1 & 1 & 1 & 0 \\\hline
Load literal & lit & 1 & 1 & 1 & 1
\end{tabular}
}
\caption{Instruction set\label{fig:instr:instr-set}}
\end{table}
The instructions are now described. For this we define an auxiliary function
$\incpcop$, which increments the program counter:
$$\incpc{k}{\mem} = \update{\mem}{\pc\mapsto\mem.\pc+k}$$
\subsubsection{Arithmetical}
\begin{align*}
\instr{\texttt{0000}}{\prog,\mem} &\eqdef
\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1+\mem.\acc2}} \\
\instr{\texttt{0001}}{\prog,\mem} &\eqdef
\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1-\mem.\acc2}}
\end{align*}
\subsubsection{Rotating and Shifting}
\begin{align*}
\instr{\texttt{0010}}{\prog,\mem} &\eqdef
\incpc1{\update{\mem}{\acc1\mapsto\rol(\mem.\acc1)}} \\
\instr{\texttt{0011}}{\prog,\mem} &\eqdef
\incpc1{\update{\mem}{\acc1\mapsto\shl(\mem.\acc1)}}
\end{align*}
\subsubsection{Logical operations}
\begin{align*}
\instr{\texttt{0100}}{\prog,\mem} &\eqdef
\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1 \land \mem.\acc2}} \\
\instr{\texttt{0101}}{\prog,\mem} &\eqdef
\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1 \lor \mem.\acc2}} \\
\instr{\texttt{0110}}{\prog,\mem} &\eqdef
\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1 \oplus \mem.\acc2}} \\
\instr{\texttt{0111}}{\prog,\mem} &\eqdef
\incpc1{\update{\mem}{\acc1\mapsto\lnot(\mem.\acc1)}}
\end{align*}
\subsubsection{Conditional jump}
$$
\instr{\texttt{1110}}{\prog,\mem} \eqdef
\begin{cases}
\update{\mem}{\pc\mapsto\mem.\acc2} & \text{if $\mem.\acc1\neq0$}\\
\incpc1{\mem} & \text{otherwise}
\end{cases}
$$
\subsubsection{Store register}
$$
\instr{\texttt{1100}}{\prog,\mem} \eqdef
\incpc1{\update{\mem}{\mem.\acc2\mapsto\mem.\acc1}}
$$
\subsubsection{Load register}
$$
\instr{\texttt{1101}}{\prog,\mem} \eqdef
\incpc1{\update{\mem}{\acc1\mapsto\mem.(\mem.\acc2)}}
$$
\subsubsection{Load literal}
\begin{align*}
\instr{\texttt{1111}}{\prog,\mem} &\eqdef
\incpc3{\update{\mem}{\acc1\mapsto(\prog.(\mem.\pc+1)\ll4)\lor(\prog.(\mem.\pc+2))}} \\
\end{align*}
|
