Changeset 524

Timestamp:

Feb 15, 2011, 5:26:53 PM (8 years ago)

Author:

mulligan

Message:

Finished discussion of anatomy of emulator

File:

• Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) (2 diffs)

Deliverables/D4.1/ITP-Paper/itp-2011.tex

@@ -315 +315 @@
 % SECTION                                                                      %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Emulator architecture}
-\label{subsect.emulator.architecture}
+\subsection{Anatomy of the (Matita) emulator}
+\label{subsect.anatomy.matita.emulator}
 
 The internal state of our Matita emulator is represented as a record:
@@ -337 +337 @@
 One peculiarity is the packing of the 24 combined SFRs into fixed length vectors.
 This was due to a bug in Matita when we were constructing the emulator, since fixed, where the time needed to typecheck a record grew exponentially with the number of fields.
+
+Both the Matita and O'Caml emulators follows the classic `fetch-decode-execute' model of processor operation.
+The most important functions in the Matita emulator are highlighted below.
+\begin{quote}
+\begin{lstlisting}
+definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat := ...
+\end{lstlisting}
+\end{quote}
+The next instruction, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
+An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned.
+These costs are taken from a Siemen's data sheet for the MCS-51, and will likely vary across manufacturers and particular derivatives of the processor.
+\begin{quote}
+\begin{lstlisting}
+definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ...
+\end{lstlisting}
+\end{quote}
+A single instruction is assembled into its corresponding bit encoding with \texttt{assembly1}:
+\begin{quote}
+\begin{lstlisting}
+definition assembly1: instruction $\rightarrow$ list Byte := ...
+\end{lstlisting}
+\end{quote}
+An assembly program, consisting of a preamble containing global data, and a list of (pseudo)instructions, is assembled using \texttt{assembly}.
+Pseudoinstructions and labels are eliminated in favour of concrete instructions from the MCS-51 instruction set.
+A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is also produced.
+\begin{quote}
+\begin{lstlisting}
+definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ...
+\end{lstlisting}
+\end{quote}
+A single execution step of the processor is evaluated using \texttt{execute\_1}, mapping a \texttt{Status} to a \texttt{Status}:
+\begin{quote}
+\begin{lstlisting}
+definition execute_1: Status → Status := ...
+\end{lstlisting}
+\end{quote}
+Multiple steps of processor execution are implemented in \texttt{execute}, which wraps \texttt{execute\_1}:
+\begin{quote}
+\begin{lstlisting}
+let rec execute (n: nat) (s: Status) on n: Status := ...
+\end{lstlisting}
+\end{quote}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%