Update instruction setHEADmaster

3 files changed, 57 insertions, 47 deletions

diff --git a/doc/chip.sty b/doc/chip.sty
index 56d061a..36ebc70 100644
--- a/doc/chip.sty
+++ b/doc/chip.sty
@@ -4,7 +4,7 @@
 \def\instr#1#2{\instrop(#1)(#2)}
 
 \def\incpcop{\mathit{incpc}}
-\def\incpc#1{\incpcop(#1)}
+\def\incpc#1#2{\incpcop_#1(#2)}
 
 \def\update#1#2{#1[#2]}
 
@@ -23,7 +23,5 @@
 \def\pc{\mathit{pc}}
 \def\acc#1{\mathit{acc}_#1}
 
-\def\nandop{\mathit{nand}}
-\def\nand#1#2{\nandop\left(#1,#2\right)}
-\def\xnorop{\mathit{xnor}}
-\def\xnor#1#2{\xnorop\left(#1,#2\right)}
+\DeclareMathOperator{\rol}{rol}
+\DeclareMathOperator{\shl}{shl}
diff --git a/doc/comp.tex b/doc/comp.tex
index 70dc2e5..c3c1f74 100644
--- a/doc/comp.tex
+++ b/doc/comp.tex
@@ -3,7 +3,7 @@ Our chip consists of the following static components:
 
 \begin{itemize}
 	\item An ALU: $\ALUOp \times \Word8 \times \Word8 \to \Word8$.
-	\item The program memory $\prog$: $\Prog \eqdef \Word6^{256}$.
+	\item The program memory $\prog$: $\Prog \eqdef \Word4^{256}$.
 \end{itemize}
 
 And these volatile components:
@@ -25,5 +25,5 @@ And these volatile components:
 \end{itemize}
 
 A state $\st$ can be seen as a tuple $(\prog,\mem)$. We define the set of all
-states $\State \eqdef \Word6^{256} \times \Word8^{256}$. An instruction is a
+states $\State \eqdef \Word4^{256} \times \Word8^{256}$. An instruction is a
 function $\Mem\to\Mem$. The instruction cycle is a function $\State\to\State$.
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*}