Changeset 396


Ignore:
Timestamp:
Dec 9, 2010, 4:47:13 PM (9 years ago)
Author:
mulligan
Message:

More changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Report/report.tex

    r395 r396  
    138138An open source emulator for the processor, MCU8051 IDE, is also available.
    139139
     140\begin{figure}[t]
     141\begin{center}
     142\includegraphics[scale=0.5]{memorylayout.png}
     143\end{center}
     144\caption{High level overview of the 8051 memory layout}
     145\label{fig.memory.layout}
     146\end{figure}
     147
    140148The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
    141149A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}.
     
    176184The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
    177185Similarly, `exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags.
    178 
    179 \begin{figure}[t]
    180 \begin{center}
    181 \includegraphics[scale=0.5]{memorylayout.png}
    182 \end{center}
    183 \caption{High level overview of the 8051 memory layout}
    184 \label{fig.memory.layout}
    185 \end{figure}
    186186
    187187\begin{figure}[t]
     
    288288
    289289The first stage consists of iterating over an assembly program, building a dictionary of all labels and their position in the program.
     290This dictionary is stored, and can later be used by the callback function passed to \texttt{execute}, the function that executes an 8051 assembly program, in order to produce a trace of labels.
     291
    290292The second stage consists of iterating over the same program and replacing all pseudojumps (both conditional and unconditional) with an 8051 jump to the requisite computed offset.
    291293One subtletly persists, however.
     
    328330Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
    329331We do not implement these functions in the Matita emulator, as Matita provides no means of input or output.
     332
     333Further, we do not implement the pseudoinstructions present in the O'Caml emulator.
     334The emulator accepts only `pure' 8051 assembly instructions.
    330335
    331336\subsection{Auxilliary data structures and libraries}
     
    512517\label{subsect.matita.validation}
    513518
    514 The Matita emulator is executable from within Matita (naturally, the speed of execution is only a fraction of the speed of the O'Caml emulator).
     519Two means of validating the Matita emulator exist.
     520
     521The emulator is executable from within Matita (naturally, the speed of execution is only a fraction of the speed of the O'Caml emulator).
    515522In particular, we provide a function \texttt{execute\_trace} which executes a fixed number of steps of an 8051 assembly program, returning a trace of the instructions executed, in the form of a list.
    516523This trace may then be compared with the trace produced by the O'Caml emulator when executing a program for validation purposes.
     524
     525Alternatively, once the Matita emulator is ported to the newest version of Matita (see Subsection~\ref{subsect.future.work}) an executable O'Caml emulator can be extracted from the Matita code, and execution traces of the extracted and prototype O'Caml emulators can be compared side-by-side.
    517526
    518527\subsection{Future work}
Note: See TracChangeset for help on using the changeset viewer.