source: Deliverables/D1.1/Presentations/WP4-dominic-presentation.tex @ 616

Last change on this file since 616 was 616, checked in by mulligan, 9 years ago

More changes.

File size: 2.9 KB
Line 
1\documentclass{beamer}
2
3\usetheme{Frankfurt}
4\logo{\includegraphics[height=1.0cm]{fetopen.png}}
5
6\usepackage[english]{babel}
7\usepackage{inputenc}
8
9\author{Dominic P. Mulligan and Claudio Sacerdoti Coen}
10\title{CerCo Work Package 4}
11\date{March 11, 2011}
12
13\begin{document}
14
15\begin{frame}
16\maketitle
17\end{frame}
18
19\begin{frame}
20\frametitle{Work Package 4}
21\end{frame}
22
23\begin{frame}
24\frametitle{The MCS-51 microprocessor I}
25\begin{itemize}
26\item
27MCS-51 is our target processor.
28Commonly called the 8051 (has an immediate successor in the 8052).
29\item
30A popular 8-bit microprocessor introduced by Intel in the late 1970s.
31\item
32Still widely used in embedded systems, and widely manufactured (including within the EU).
33\item
34Is a relatively simple microprocessor especially suited to CerCo's aims.
35\item
36We can accurately predict how long an instruction will take to execute in cycles (i.e. no pipelining, caching etc.)
37We use timings from a Siemen's datasheet.
38Vary between manufacturers and models.
39\end{itemize}
40\end{frame}
41
42\begin{frame}
43\frametitle{The MCS-51 microprocessor II}
44\begin{itemize}
45\item
46I will not give an exhaustive introduction to the processor.
47I am going to reveal enough for you to understand what problems we faced in formalising it.
48\item
49The MCS-51 has a byzantine memory model.
50\item
51Memory spaces overlap, have different sizes, may not be present depending on model, can be addressed in multiple ways, and addressed with different sized pointers.
52\item
53Instruction set is non-orthogonal.
54For instance, \texttt{MOV} can take 16 combinations of addressing mode out of a possible 300+.
55\end{itemize}
56\end{frame}
57
58\begin{frame}
59\frametitle{The MCS-51 microprocessor III}
60\begin{itemize}
61\item
62Instruction set contains three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used).
63\item
64These differ in the size of permissible offset and the size in bytes of instruction.
65\item
66MCS-51 also has various timers, UART I/O and interrupts.
67Succesor 8052 adds additional timers.
68\item
69Interrupts are simpler than a modern processor, as flags can be used to manually handle errors.
70\end{itemize}
71\end{frame}
72
73\begin{frame}
74\frametitle{Development strategy}
75We built two emulators for the processor.
76\vspace{1em}
77The first was written in O'Caml.
78This allowed us to `iron out' issues in the design and implementation, and make rapid changes in O'Caml's more permissive type system.
79We made use of O'Caml's ability to perform I/O for debugging purposes.
80\vspace{1em}
81When we were happy with the O'Caml emulator, we moved to Matita.
82Matita's language is lexically similar to O'Caml, so swathes of code could be copy-pasted with little additional effort.
83\end{frame}
84
85\begin{frame}
86\frametitle{Problems to be solved}
87\end{frame}
88
89\begin{frame}
90\frametitle{Polymorphic variants and phantom types}
91\end{frame}
92
93\begin{frame}
94\frametitle{Use of dependent types}
95\end{frame}
96
97\end{document}
Note: See TracBrowser for help on using the repository browser.