Changeset 628


Ignore:
Timestamp:
Mar 3, 2011, 3:41:36 PM (9 years ago)
Author:
mulligan
Message:

Finished slides.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.1/Presentations/WP4-dominic-presentation.tex

    r620 r628  
    187187\frametitle{Overlapping memory spaces and addressing modes}
    188188MCS-51 memory spaces overlap, and can be addressed using different modes and sized pointers.
    189 The status record models memory merely as disjoint spaces, using a `tries with holes' datastructure.
    190 
    191 All complications to do with overlapping are handled
     189The `status' record models memory merely as disjoint spaces, using a `tries with holes' datastructure.
     190
     191All complications to do with overlapping are handled by \texttt{set\_arg\_XX} and \texttt{get\_arg\_XX} for \texttt{XX} = 1, 8, 16.
     192These functions make use of the aforementioned dependent type trick.
     193\end{frame}
     194
     195\begin{frame}
     196\frametitle{Validation}
     197We worked hard to make sure we implemented a MCS-51 emulator:
     198\begin{itemize}
     199\item
     200Multiple data sheets from different manufacturers (errors found!)
     201\item
     202O'Caml output to Intel HEX for loading into third party tools, and input for use with SDCC.
     203\item
     204O'Caml produced trace files with processor status after every execution step, every opcode tested.
     205\item
     206Matita formalisation is also executable, and traces can be compared with O'Caml.
     207\end{itemize}
    192208\end{frame}
    193209
Note: See TracChangeset for help on using the changeset viewer.