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

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

More work on slides.

File size: 4.1 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{Dealing with the jumps}
89\begin{itemize}
90\item
91Unconditional jumps a problem, as offset has to be computed ahead of time.
92\item
93This is problematic for separate compilation, and also for prototype C compiler.
94\item
95Much better to implement pseudoinstructions which are `assembled away'.
96\item
97Introduce labels and cost labels (for cost traces).
98\item
99Then introduce pseudoinstructions like \texttt{Jump} for unconditional jumping to labels: no offset calculation required beforehand.
100\item
101Other pseudoinstructions introduced: \texttt{Mov} for moving arbitrary (16 bit) data stored at a label (global vars) and conditional jumps to labels.
102\item
103Our assembly language similar to that of SDCC.
104\end{itemize}
105\end{frame}
106
107\begin{frame}
108\frametitle{Polymorphic variants and phantom types}
109\begin{itemize}
110\item
111The instruction set is highly non-orthogonal.
112\item
113We needed a way of
114\end{itemize}
115\end{frame}
116
117\begin{frame}
118\frametitle{Use of dependent types}
119\end{frame}
120
121\begin{frame}
122\frametitle{What is implemented}
123In O'Caml we implemented the emulator proper, associated assembler, supprting debugging code (for loading and outputting Intel HEX), and also have (untested) code for timers, interrupts and I/O.
124
125In Matita, we have the emulator proper and associated assembler.
126We have yet to port the timers and I/O, preferring to focus on the core emulator.
127\end{frame}
128
129\begin{frame}
130\frametitle{Demo}
131\end{frame}
132
133\end{document}
Note: See TracBrowser for help on using the repository browser.