Changeset 524

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

Finished discussion of anatomy of emulator

1 edited


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

    r523 r524  
    315315% SECTION                                                                      %
    317 \subsection{Emulator architecture}
    318 \label{subsect.emulator.architecture}
     317\subsection{Anatomy of the (Matita) emulator}
    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.
     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.
     344definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat := ...
     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.
     352definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ...
     355A single instruction is assembled into its corresponding bit encoding with \texttt{assembly1}:
     358definition assembly1: instruction $\rightarrow$ list Byte := ...
     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.
     366definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ...
     369A single execution step of the processor is evaluated using \texttt{execute\_1}, mapping a \texttt{Status} to a \texttt{Status}:
     372definition execute_1: Status → Status := ...
     375Multiple steps of processor execution are implemented in \texttt{execute}, which wraps \texttt{execute\_1}:
     378let rec execute (n: nat) (s: Status) on n: Status := ...
Note: See TracChangeset for help on using the changeset viewer.