Changeset 377 for Deliverables


Ignore:
Timestamp:
Dec 6, 2010, 11:44:23 AM (9 years ago)
Author:
mulligan
Message:

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

File:
1 edited

Legend:

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

    r376 r377  
    177177Once 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.
    178178
     179\subsection{Lack of orthogonality in instruction set}
     180\label{subsect.lack.orthogonality.instruction.set}
     181
     182\subsection{Pseudo-instructions}
     183\label{subsect.pseudo-instructions}
     184
     185In validating the design and implementation of the O'Caml emulator we used two tactics:
     186\begin{enumerate}
     187\item
     188Use 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).
     189We found typographic errors in manufacturer's data sheets which were resolved by consulting an alternative sheet.
     190\item
     191Use of reference compilers and emulators.
     192The operation of the emulator was manually tested by reference to \textsc{mcu 8051 ide}, an emulator for the 8051 series processor.
     193A 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}.
     194The status changes in both emulators were then compared.
     195
     196For 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.
     197\end{enumerate}
     198
     199As 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}.
     200
     201\subsection{Validation}
     202\label{subsect.validation}
     203
    179204\section{The emulator in Matita}
    180205\label{sect.emulator.in.matita}
    181206
    182 \subsection{What we implement}
    183 \label{subsect.what.we.implement}
     207\subsection{What we do not implement}
     208\label{subsect.what.we.do.not.implement}
    184209
    185210Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
     
    191216A small library of data structures was written, along with basic functions operating over them.
    192217Implemented data structures include: Booleans, option types, lists, Cartesian products, Natural numbers, fixed-length vectors, and sparse tries.
     218
     219Our type of vectors, in particular, makes heavy use of dependent types.
     220Probing vectors is `type safe' for instance: we cannot index into a vector beyond the vector's length.
    193221
    194222We represent bits as Boolean values.
     
    215243We probe a trie with the \texttt{lookup} function.
    216244This takes an additional argument representing the value to be returned should a stub, representing uninitialised data, be encountered during traversal.
     245
     246Like the O'Caml emulator, we use a record to represent processor state:
    217247
    218248\begin{quote}
     
    230260  special_function_registers_8052: Vector Byte five;
    231261 
    232   p1_latch: Byte;
    233   p3_latch: Byte;
    234  
    235   clock: Time
     262  ...
    236263}.
    237264\end{lstlisting}
    238265\end{quote}
    239266
    240 % Polymorphic variants
    241 
    242 % Parsing
    243 
    244 % Bitvectors: dependent types
    245 
    246 % Dependent types subtyping
     267However, 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.
     268We then provide functions that index into the respective vector to `get' and `set' the respective SFRs.
     269This is due to record typechecking in Matita being slow for large records.
     270
     271\subsection{Addressing modes: use of dependent types}
     272\label{subsect.addressing.modes.use.of.dependent.types}
    247273
    248274\subsection{Dealing with partiality}
Note: See TracChangeset for help on using the changeset viewer.