source: Deliverables/D4.1/Report/report.tex @ 376

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

Work on describing sparse bitvector tries.

File size: 11.2 KB
Line 
1\documentclass[11pt, epsf, a4wide]{article}
2
3\usepackage{../../style/cerco}
4
5\usepackage{amsfonts}
6\usepackage{amsmath}
7\usepackage{amssymb} 
8\usepackage[english]{babel}
9\usepackage[utf8x]{inputenc}
10\usepackage{listings}
11\usepackage{url}
12
13\title{
14INFORMATION AND COMMUNICATION TECHNOLOGIES\\
15(ICT)\\
16PROGRAMME\\
17\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
18
19\lstdefinelanguage{matita}
20  {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,Type},
21   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
22   mathescape=true,
23  }
24
25\lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false,
26        keywordstyle=\color{red}\bfseries,
27        keywordstyle=[2]\color{blue},
28        commentstyle=\color{green},
29        stringstyle=\color{blue},
30        showspaces=false,showstringspaces=false}
31
32\lstset{extendedchars=false}
33\lstset{inputencoding=utf8x}
34\DeclareUnicodeCharacter{8797}{:=}
35\DeclareUnicodeCharacter{10746}{++}
36\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
37\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
38
39\date{}
40\author{}
41
42\begin{document}
43
44\thispagestyle{empty}
45
46\vspace*{-1cm}
47\begin{center}
48\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
49\end{center}
50
51\begin{minipage}{\textwidth}
52\maketitle
53\end{minipage}
54
55\vspace*{0.5cm}
56\begin{center}
57\begin{LARGE}
58\textbf{
59Report n. D4.1\\
60Intel 8051/8052 emulator prototype, and formalisation in Matita}
61\end{LARGE} 
62\end{center}
63
64\vspace*{2cm}
65\begin{center}
66\begin{large}
67Version 1.0
68\end{large}
69\end{center}
70
71\vspace*{0.5cm}
72\begin{center}
73\begin{large}
74Main Authors:\\
75Claudio Sacerdoti Coen and Dominic P. Mulligan
76\end{large}
77\end{center}
78
79\vspace*{\fill}
80
81\noindent
82Project Acronym: \cerco{}\\
83Project full title: Certified Complexity\\
84Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
85
86\clearpage
87\pagestyle{myheadings}
88\markright{\cerco{}, FP7-ICT-2009-C-243881}
89
90\newpage
91
92\vspace*{7cm}
93\paragraph{Abstract}
94We discuss the design and implementation of an O'Caml emulator for the Intel 8051/8052 eight bit processor, and its subsequent formalisation in the dependently typed proof assistant Matita.
95
96\newpage
97
98\tableofcontents
99
100\newpage
101
102\section{Introduction}
103\label{sect.introduction}
104
105\subsection{Task}
106\label{subsect.task}
107
108\subsection{A brief overview of the target processor}
109\label{subsect.brief.overview.target.processor}
110
111\begin{figure}
112\caption{High level overview of the 8051 memory layout}
113\label{fig.memory.layout}
114\end{figure}
115
116The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
117Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
118Further, the processor and its immediate successor, the 8052, is still manufactured by a host of semiconductor suppliers---many of them European---including Atmel, Siemens Semiconductor, NXP (formerly Phillips Semiconductor), Texas Instruments, and Maxim (formerly Dallas Semiconductor).
119
120The 8051 is a well documented processor, and has the additional support of numerous open source and commercial tools, such as compilers for high-level languages and emulators.
121For instance, the open source Small Device C Compiler (SDCC) recognises a dialect of C, and other compilers targeting the 8051 for BASIC, Forth and Modula-2 are also extant.
122An open source emulator for the processor, MCU8051 IDE, is also available.
123
124% Processor architecture
125The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
126A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}.
127
128% Internal RAM
129Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
130Internal memory, commonly provided on the die itself with fast access, is further divided into 128 bytes of internal RAM and numerous Special Function Registers (SFRs) which control the operation of the processor.
131Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7).
132These sit in the first eight bytes of IRAM, though can be programmatically `shifted up' as needed.
133Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks.
134What remains of the IRAM may be treated as general purpose memory.
135
136% External RAM
137External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
138XRAM is accessed using a dedicated instruction.
139External code memory is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
140However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code may also be supplied (the processor has a Harvard architecture, where program code and data are separated).
141
142% ALU
143The 8051 series possesses an eight bit Arithmetic and Logic Unit (ALU), with a wide variety of instructions for performing arithmetic and logical operations on bits and integers.
144Further, the processor possesses two eight bit general purpose accumulators, A and B.
145
146% Serial I/O and the input-output lines
147Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
148Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation.
149(The 8052 provides an additional sixteen bit timer.)
150As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
151
152%
153The programmer may take advantage of the interrupt mechanism that the processor provides.
154This is especially useful when dealing with input or output involving the serial device, as an interrupt can be set when a whole character is sent or received via the serial port.
155
156Interrupts immediately halt the flow of execution of the processor, and cause the program counter to jump to a fixed address, where the requisite interrupt handler is stored.
157However, interrupts may be set to one of two priorities: low and high.
158The interrupt handler of an interrupt with high priority is executed ahead of the interrupt handler of an interrupt of lower priority, interrupting a currently executing handler of lower priority, if necessary.
159
160The 8051 has interrupts disabled by default.
161The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
162Similarly, `exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags.
163
164\section{The emulator in O'Caml}
165\label{sect.emulator.in.ocaml}
166
167\subsection{Anatomy of the emulator}
168\label{subsect.anatomy.emulator}
169
170We provide a high-level overview of the operation of the emulator.
171
172% Intel HEX, parsing
173Program code is loaded onto the 8051 in a standard format, the Intel Hex (IHX) format.
174All compilers producing machine code for the 8051, including the SDCC compiler which we use for debugging purposes, produce compiled programs in IHX format as standard.
175Accordingly, our O'Caml emulator can parse IHX files and populate the emulator's code memory with their contents.
176
177Once code memory is populated, and the rest of the emulator state has been initialised (i.e. setting the program counter to zero), the O'Caml emulator fetches the instruction pointed to by the program counter from code memory.
178
179\section{The emulator in Matita}
180\label{sect.emulator.in.matita}
181
182\subsection{What we implement}
183\label{subsect.what.we.implement}
184
185Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
186We do not implement these functions in the Matita emulator, as Matita provides no means of input or output.
187
188\subsection{Auxilliary data structures and libraries}
189\label{subsect.auxilliary.data.structures.and.libraries}
190
191A small library of data structures was written, along with basic functions operating over them.
192Implemented data structures include: Booleans, option types, lists, Cartesian products, Natural numbers, fixed-length vectors, and sparse tries.
193
194We represent bits as Boolean values.
195Nibbles, bytes, words, and so on, are represented as fixed length (bit)vectors of the requisite length.
196
197\subsection{The emulator state}
198\label{subsect.emulator.state}
199
200We represent all processor memory in the Matita emulator as a sparse (bitvector)trie:
201
202\begin{quote}
203\begin{lstlisting}
204ninductive BitVectorTrie (A: Type[0]): Nat $\rightarrow$ Type[0] ≝
205  Leaf: A $\rightarrow$ BitVectorTrie A Z
206| Node: ∀n: Nat. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
207| Stub: ∀n: Nat. BitVectorTrie A n.
208\end{lstlisting}
209\end{quote}
210
211Nodes are addressed by a bitvector index, representing a path through the tree.
212At any point in the tree, a \texttt{Stub} may be inserted, representing a `hole' in the tree.
213All functions operating on tries use dependent types to enforce the invariant that the height of the tree and the length of the bitvector representing a path through the tree are the same.
214
215We probe a trie with the \texttt{lookup} function.
216This takes an additional argument representing the value to be returned should a stub, representing uninitialised data, be encountered during traversal.
217
218\begin{quote}
219\begin{lstlisting}
220nrecord Status: Type[0] ≝
221{
222  code_memory: BitVectorTrie Byte sixteen;
223  low_internal_ram: BitVectorTrie Byte seven;
224  high_internal_ram: BitVectorTrie Byte seven;
225  external_ram: BitVectorTrie Byte sixteen;
226 
227  program_counter: Word;
228 
229  special_function_registers_8051: Vector Byte nineteen;
230  special_function_registers_8052: Vector Byte five;
231 
232  p1_latch: Byte;
233  p3_latch: Byte;
234 
235  clock: Time
236}.
237\end{lstlisting}
238\end{quote}
239
240% Polymorphic variants
241
242% Parsing
243
244% Bitvectors: dependent types
245
246% Dependent types subtyping
247
248\subsection{Dealing with partiality}
249\label{subsect.dealing.with.partiality}
250
251The O'Caml 8051 emulator makes use of a number of partial functions.
252These functions either \texttt{assert false}\footnote{O'Caml idiom: immediately halts execution of the running program.} or do not perform a comprehensive pattern analysis over their inputs.
253There are a number of possible reasons for this:
254\begin{enumerate}
255\item
256\textbf{Incomplete pattern analyses} are used where we are confident that the particular pattern match in question should never occur, for instance if the calling function performs a test beforehand, or where the emulator should fail anyway if a particular unchecked pattern is used as input.
257An example of a function which exhibits the latter behaviour is \texttt{set\_arg\_16} from \texttt{ASMInterpret.ml}, which fails with a pattern match exception if called on an input representing an eight bit argument.
258\item
259\textbf{Assert false} may be called if the emulator finds itself in an `impossible situation'.
260In this respect, we used \texttt{assert false} in a similar way to the previously described use of incomplete pattern analysis.
261\item
262\textbf{Assert false} may be called is some feature of the physical 8051 processor is not implemented in the O'Caml emulator and an executing program is attempting to use it.
263\end{enumerate}
264\end{document}
Note: See TracBrowser for help on using the repository browser.