From bc939202c19c43b86eb8c804432e7af09547a934 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Wed, 22 Jun 2016 17:50:40 +0200
Subject: Initial commit

---
 doc/instr.tex | 85 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 85 insertions(+)
 create mode 100644 doc/instr.tex

(limited to 'doc/instr.tex')

diff --git a/doc/instr.tex b/doc/instr.tex
new file mode 100644
index 0000000..4bc27e0
--- /dev/null
+++ b/doc/instr.tex
@@ -0,0 +1,85 @@
+\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}{\mem})$$
+
+Here, $\instrop$ is a function that maps words to instructions: $\instrop :
+\Word6 \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]
+	\centering
+	{\tt
+	\begin{tabular}{!>{\normalfont}l | ^l | *{6}{|^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$} \\
+	\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{\mem} = \update{\mem}{\pc\mapsto\mem.\pc+1}$$
+
+\subsubsection{Addition}
+$$
+	\instr{\texttt{100000}}{\mem} \eqdef
+	\incpc{\update{\mem}{\acc1\mapsto\mem.\acc1+\mem.\acc2}}
+$$
+
+\subsubsection{Logical NAND}
+$$
+	\instr{\texttt{100001}}{\mem} \eqdef
+	\incpc{\update{\mem}{\acc1\mapsto\nand{\mem.\acc1}{\mem.\acc2}}}
+$$
+
+\subsubsection{Equality}
+$$
+	\instr{\texttt{100001}}{\mem} \eqdef
+	\incpc{\update{\mem}{\acc1\mapsto\xnor{\mem.\acc1}{\mem.\acc2}}}
+$$
+
+\subsubsection{Conditional jump}
+$$
+	\instr{\texttt{110000}}{\mem} \eqdef
+	\begin{cases}
+		\update{\mem}{\pc\mapsto\mem.\acc2} & \text{if $\mem.\acc1\neq0$}\\
+		\incpc{\mem} & \text{otherwise}
+	\end{cases}
+$$
+
+\subsubsection{Store register}
+$$
+	\instr{\texttt{111110}}{\mem} \eqdef
+	\incpc{\update{\mem}{\mem.\acc2\mapsto\mem.\acc1}}
+$$
+
+\subsubsection{Load register}
+$$
+	\instr{\texttt{111111}}{\mem} \eqdef
+	\incpc{\update{\mem}{\acc1\mapsto\mem.(\mem.\acc2)}}
+$$
+
+\subsubsection{Store 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)}}
+\end{align*}
-- 
cgit v1.2.3