Changeset 396 for Deliverables

Dec 9, 2010, 4:47:13 PM (11 years ago)

More changes.

1 edited


  • Deliverables/D4.1/Report/report.tex

    r395 r396  
    138138An open source emulator for the processor, MCU8051 IDE, is also available.
     144\caption{High level overview of the 8051 memory layout}
    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.
    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}
    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.
    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.
     333Further, we do not implement the pseudoinstructions present in the O'Caml emulator.
     334The emulator accepts only `pure' 8051 assembly instructions.
    331336\subsection{Auxilliary data structures and libraries}
    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.
     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.
     525Alternatively, once the Matita emulator is ported to the newest version of Matita (see Subsection~\ref{}) 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.
    518527\subsection{Future work}
Note: See TracChangeset for help on using the changeset viewer.