# Changeset 396

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

More changes.

File:
1 edited

### Legend:

Unmodified
 r395 An open source emulator for the processor, MCU8051 IDE, is also available. \begin{figure}[t] \begin{center} \includegraphics[scale=0.5]{memorylayout.png} \end{center} \caption{High level overview of the 8051 memory layout} \label{fig.memory.layout} \end{figure} The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation. A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}. The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs. Similarly, exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags. \begin{figure}[t] \begin{center} \includegraphics[scale=0.5]{memorylayout.png} \end{center} \caption{High level overview of the 8051 memory layout} \label{fig.memory.layout} \end{figure} \begin{figure}[t] The first stage consists of iterating over an assembly program, building a dictionary of all labels and their position in the program. This 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. The 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. One subtletly persists, however. Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files. We do not implement these functions in the Matita emulator, as Matita provides no means of input or output. Further, we do not implement the pseudoinstructions present in the O'Caml emulator. The emulator accepts only pure' 8051 assembly instructions. \subsection{Auxilliary data structures and libraries} \label{subsect.matita.validation} 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). Two means of validating the Matita emulator exist. The emulator is executable from within Matita (naturally, the speed of execution is only a fraction of the speed of the O'Caml emulator). In 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. This trace may then be compared with the trace produced by the O'Caml emulator when executing a program for validation purposes. Alternatively, 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. \subsection{Future work}