Changeset 377 for Deliverables

Timestamp:

Dec 6, 2010, 11:44:23 AM (10 years ago)

Author:

mulligan

Message:

Description of techniques related to validation of O'Caml emulator.

File:

• Deliverables/D4.1/Report/report.tex (modified) (4 diffs)

Deliverables/D4.1/Report/report.tex

@@ -177 +177 @@
 Once code memory is populated, and the rest of the emulator state has been initialised (i.e. setting the program counter to zero), the O'Caml emulator fetches the instruction pointed to by the program counter from code memory.
 
+\subsection{Lack of orthogonality in instruction set}
+\label{subsect.lack.orthogonality.instruction.set}
+
+\subsection{Pseudo-instructions}
+\label{subsect.pseudo-instructions}
+
+In validating the design and implementation of the O'Caml emulator we used two tactics:
+\begin{enumerate}
+\item
+Use of multiple manufacturer's data sheets (both the Siemens Semiconductor and Phillips Semiconductor specifications for the 8051, as well as online sources such as the Keil website).
+We found typographic errors in manufacturer's data sheets which were resolved by consulting an alternative sheet.
+\item
+Use of reference compilers and emulators.
+The operation of the emulator was manually tested by reference to \textsc{mcu 8051 ide}, an emulator for the 8051 series processor.
+A number of small C programs were compiled in SDCC\footnote{See the \texttt{GCC} directory for a selection of them.}, and the resulting IHX files were disassembled by \textsc{mcu 8051 ide}.
+The status changes in both emulators were then compared.
+
+For further validation, the output of the compiled C programs from SDCC was compared with the output of the same programs in GCC, in order to pre-empt the introduction of bugs in the emulator inherited from a faulty C compiler.
+\end{enumerate}
+
+As a further check, the design and operation of the emulator was compared with the textual description of online tutorials on 8051 programming, such as those found at \url{http://www.8052.com}.
+
+\subsection{Validation}
+\label{subsect.validation}
+
 \section{The emulator in Matita}
 \label{sect.emulator.in.matita}
 
-\subsection{What we implement}
-\label{subsect.what.we.implement}
+\subsection{What we do not implement}
+\label{subsect.what.we.do.not.implement}
 
 Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
@@ -191 +216 @@
 A small library of data structures was written, along with basic functions operating over them.
 Implemented data structures include: Booleans, option types, lists, Cartesian products, Natural numbers, fixed-length vectors, and sparse tries.
+
+Our type of vectors, in particular, makes heavy use of dependent types.
+Probing vectors is `type safe' for instance: we cannot index into a vector beyond the vector's length.
 
 We represent bits as Boolean values.
@@ -215 +243 @@
 We probe a trie with the \texttt{lookup} function.
 This takes an additional argument representing the value to be returned should a stub, representing uninitialised data, be encountered during traversal.
+
+Like the O'Caml emulator, we use a record to represent processor state:
 
 \begin{quote}
@@ -230 +260 @@
   special_function_registers_8052: Vector Byte five;
   
-  p1_latch: Byte;
-  p3_latch: Byte;
-  
-  clock: Time
+  ...
 }.
 \end{lstlisting}
 \end{quote}
 
-% Polymorphic variants
-
-% Parsing
-
-% Bitvectors: dependent types
-
-% Dependent types subtyping
+However, we `squash' the \texttt{Status} record in the Matita emulator by grouping all 8051 SFRs (respectively, 8052 SFRs) into a single vector of bytes, as opposed to representing them as explicit fields in the record itself.
+We then provide functions that index into the respective vector to `get' and `set' the respective SFRs.
+This is due to record typechecking in Matita being slow for large records.
+
+\subsection{Addressing modes: use of dependent types}
+\label{subsect.addressing.modes.use.of.dependent.types}
 
 \subsection{Dealing with partiality}