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

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

Fixed layout.

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