From 3019b3684d0d94f318f719bfdd5163e84d9e91b0 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Thu, 23 Jun 2016 14:47:40 +0200
Subject: Update instruction set

---
 doc/instr.tex | 92 +++++++++++++++++++++++++++++++++--------------------------
 1 file changed, 52 insertions(+), 40 deletions(-)

(limited to 'doc/instr.tex')

diff --git a/doc/instr.tex b/doc/instr.tex
index 4bc27e0..e9bc296 100644
--- a/doc/instr.tex
+++ b/doc/instr.tex
@@ -5,29 +5,33 @@
 The instruction cycle is a function $\State\to\State$. It is defined as
 follows:
 
-$$\mathit{cycle}(\prog,\mem) \eqdef (\prog, \instr{\mem.\pc}{\mem})$$
+$$\mathit{cycle}(\prog,\mem) \eqdef (\prog, \instr{\mem.\pc}{\prog,\mem})$$
 
 Here, $\instrop$ is a function that maps words to instructions: $\instrop :
-\Word6 \to \Mem \to \Mem$. It is defined in \autoref{sec:instr}.
+\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}[b]
+\begin{table}[h]
 	\centering
 	{\tt
-	\begin{tabular}{!>{\normalfont}l | ^l | *{6}{|^c}}
+	\begin{tabular}{!>{\normalfont}l | ^l | *{4}{|^c}}
 		\rowstyle{\normalfont\bfseries}
-		Instruction name & Assembly & 5 & 4 & 3 & 2 & 1 & 0 \\\hline
-		Addition         & add      & 1 & 0 & 0 & 0 & 0 & 0 \\\hline
-		Logical NAND     & nand     & 1 & 0 & 0 & 0 & 0 & 1 \\\hline
-		Equality         & eq       & 1 & 0 & 0 & 0 & 1 & 0 \\\hline
-		Conditional jump & cjmp     & 1 & 1 & 0 & 0 & 0 & 0 \\\hline
-		Store register   & str      & 1 & 1 & 1 & 1 & 1 & 0 \\\hline
-		Load register    & ld       & 1 & 1 & 1 & 1 & 1 & 1 \\\hline
-		Store literal 1  & lit1     & 0 & 0 & \multicolumn{4}{c}{$k$} \\\hline
-		Store literal 2  & lit2     & 0 & 1 & \multicolumn{4}{c}{$k$} \\
+		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}}
@@ -35,51 +39,59 @@ The binary representations of the commands defined can be found in
 
 The instructions are now described. For this we define an auxiliary function
 $\incpcop$, which increments the program counter:
-$$\incpc{\mem} = \update{\mem}{\pc\mapsto\mem.\pc+1}$$
+$$\incpc{k}{\mem} = \update{\mem}{\pc\mapsto\mem.\pc+k}$$
 
-\subsubsection{Addition}
-$$
-	\instr{\texttt{100000}}{\mem} \eqdef
-	\incpc{\update{\mem}{\acc1\mapsto\mem.\acc1+\mem.\acc2}}
-$$
+\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{Logical NAND}
-$$
-	\instr{\texttt{100001}}{\mem} \eqdef
-	\incpc{\update{\mem}{\acc1\mapsto\nand{\mem.\acc1}{\mem.\acc2}}}
-$$
+\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{Equality}
-$$
-	\instr{\texttt{100001}}{\mem} \eqdef
-	\incpc{\update{\mem}{\acc1\mapsto\xnor{\mem.\acc1}{\mem.\acc2}}}
-$$
+\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{110000}}{\mem} \eqdef
+	\instr{\texttt{1110}}{\prog,\mem} \eqdef
 	\begin{cases}
 		\update{\mem}{\pc\mapsto\mem.\acc2} & \text{if $\mem.\acc1\neq0$}\\
-		\incpc{\mem} & \text{otherwise}
+		\incpc1{\mem} & \text{otherwise}
 	\end{cases}
 $$
 
 \subsubsection{Store register}
 $$
-	\instr{\texttt{111110}}{\mem} \eqdef
-	\incpc{\update{\mem}{\mem.\acc2\mapsto\mem.\acc1}}
+	\instr{\texttt{1100}}{\prog,\mem} \eqdef
+	\incpc1{\update{\mem}{\mem.\acc2\mapsto\mem.\acc1}}
 $$
 
 \subsubsection{Load register}
 $$
-	\instr{\texttt{111111}}{\mem} \eqdef
-	\incpc{\update{\mem}{\acc1\mapsto\mem.(\mem.\acc2)}}
+	\instr{\texttt{1101}}{\prog,\mem} \eqdef
+	\incpc1{\update{\mem}{\acc1\mapsto\mem.(\mem.\acc2)}}
 $$
 
-\subsubsection{Store literal}
+\subsubsection{Load literal}
 \begin{align*}
-	\instr{\texttt{00}k}{\mem} &\eqdef
-	\incpc{\update{\mem}{\acc1\mapsto(\mem.\acc1 \land \texttt{0xf0})\lor k}} \\
-	\instr{\texttt{01}k}{\mem} &\eqdef
-	\incpc{\update{\mem}{\acc1\mapsto(\mem.\acc1 \land \texttt{0x0f})\lor (k \ll 4)}}
+	\instr{\texttt{1111}}{\prog,\mem} &\eqdef
+	\incpc3{\update{\mem}{\acc1\mapsto(\prog.(\mem.\pc+1)\ll4)\lor(\prog.(\mem.\pc+2))}} \\
 \end{align*}
-- 
cgit v1.2.3

