# Changeset 616 for Deliverables

Ignore:
Timestamp:
Mar 2, 2011, 11:40:50 AM (9 years ago)
Message:

More changes.

File:
1 edited

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

 r615 \item Is a relatively simple microprocessor especially suited to CerCo's aims. \item We can accurately predict how long an instruction will take to execute in cycles (i.e. no pipelining, caching etc.) We use timings from a Siemen's datasheet. Vary between manufacturers and models. \end{itemize} \end{frame} I am going to reveal enough for you to understand what problems we faced in formalising it. \item The MCS-51 has a byzantine memory model. \item Memory spaces overlap, have different sizes, may not be present depending on model, can be addressed in multiple ways, and addressed with different sized pointers. \item Instruction set is non-orthogonal. For instance, \texttt{MOV} can take 16 combinations of addressing mode out of a possible 300+. \end{itemize} \end{frame} \begin{frame} \frametitle{The MCS-51 microprocessor III} \begin{itemize} \item Instruction set contains three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used). \item These differ in the size of permissible offset and the size in bytes of instruction. \item MCS-51 also has various timers, UART I/O and interrupts. Succesor 8052 adds additional timers. \item Interrupts are simpler than a modern processor, as flags can be used to manually handle errors. \end{itemize} \end{frame} \begin{frame} \frametitle{Development strategy} We built two emulators for the processor. \vspace{1em} The first was written in O'Caml. This allowed us to `iron out' issues in the design and implementation, and make rapid changes in O'Caml's more permissive type system. We made use of O'Caml's ability to perform I/O for debugging purposes. \vspace{1em} When we were happy with the O'Caml emulator, we moved to Matita. Matita's language is lexically similar to O'Caml, so swathes of code could be copy-pasted with little additional effort. \end{frame}
Note: See TracChangeset for help on using the changeset viewer.