Changeset 524


Ignore:
Timestamp:
Feb 15, 2011, 5:26:53 PM (6 years ago)
Author:
mulligan
Message:

Finished discussion of anatomy of emulator

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r523 r524  
    315315% SECTION                                                                      %
    316316%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    317 \subsection{Emulator architecture}
    318 \label{subsect.emulator.architecture}
     317\subsection{Anatomy of the (Matita) emulator}
     318\label{subsect.anatomy.matita.emulator}
    319319
    320320The internal state of our Matita emulator is represented as a record:
     
    337337One peculiarity is the packing of the 24 combined SFRs into fixed length vectors.
    338338This 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.
     339
     340Both the Matita and O'Caml emulators follows the classic `fetch-decode-execute' model of processor operation.
     341The most important functions in the Matita emulator are highlighted below.
     342\begin{quote}
     343\begin{lstlisting}
     344definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat := ...
     345\end{lstlisting}
     346\end{quote}
     347The next instruction, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
     348An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned.
     349These 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.
     350\begin{quote}
     351\begin{lstlisting}
     352definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ...
     353\end{lstlisting}
     354\end{quote}
     355A single instruction is assembled into its corresponding bit encoding with \texttt{assembly1}:
     356\begin{quote}
     357\begin{lstlisting}
     358definition assembly1: instruction $\rightarrow$ list Byte := ...
     359\end{lstlisting}
     360\end{quote}
     361An assembly program, consisting of a preamble containing global data, and a list of (pseudo)instructions, is assembled using \texttt{assembly}.
     362Pseudoinstructions and labels are eliminated in favour of concrete instructions from the MCS-51 instruction set.
     363A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is also produced.
     364\begin{quote}
     365\begin{lstlisting}
     366definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ...
     367\end{lstlisting}
     368\end{quote}
     369A single execution step of the processor is evaluated using \texttt{execute\_1}, mapping a \texttt{Status} to a \texttt{Status}:
     370\begin{quote}
     371\begin{lstlisting}
     372definition execute_1: Status → Status := ...
     373\end{lstlisting}
     374\end{quote}
     375Multiple steps of processor execution are implemented in \texttt{execute}, which wraps \texttt{execute\_1}:
     376\begin{quote}
     377\begin{lstlisting}
     378let rec execute (n: nat) (s: Status) on n: Status := ...
     379\end{lstlisting}
     380\end{quote}
    339381
    340382%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.