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

Last change on this file since 371 was 371, checked in by mulligan, 10 years ago

Report started. Background/introduction finished (first draft). Starting on description of O'Caml emulator.

File size: 6.8 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{url}
10
11\title{
12INFORMATION AND COMMUNICATION TECHNOLOGIES\\
13(ICT)\\
14PROGRAMME\\
15\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
16
17\date{}
18\author{}
19
20\begin{document}
21
22\thispagestyle{empty}
23
24\vspace*{-1cm}
25\begin{center}
26\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
27\end{center}
28
29\begin{minipage}{\textwidth}
30\maketitle
31\end{minipage}
32
33\vspace*{0.5cm}
34\begin{center}
35\begin{LARGE}
36\textbf{
37Report n. D4.1\\
38Intel 8051/8052 emulator prototype, and formalisation in Matita}
39\end{LARGE} 
40\end{center}
41
42\vspace*{2cm}
43\begin{center}
44\begin{large}
45Version 1.0
46\end{large}
47\end{center}
48
49\vspace*{0.5cm}
50\begin{center}
51\begin{large}
52Main Authors:\\
53Claudio Sacerdoti Coen and Dominic P. Mulligan
54\end{large}
55\end{center}
56
57\vspace*{\fill}
58
59\noindent
60Project Acronym: \cerco{}\\
61Project full title: Certified Complexity\\
62Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
63
64\clearpage
65\pagestyle{myheadings}
66\markright{\cerco{}, FP7-ICT-2009-C-243881}
67
68\newpage
69
70\vspace*{7cm}
71\paragraph{Abstract}
72We 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.
73
74\newpage
75
76\tableofcontents
77
78\newpage
79
80\section{Introduction}
81\label{sect.introduction}
82
83\subsection{Task}
84\label{subsect.task}
85
86\subsection{A brief overview of the target processor}
87\label{subsect.brief.overview.target.processor}
88
89\begin{figure}
90\caption{High level overview of the 8051 memory layout}
91\label{fig.memory.layout}
92\end{figure}
93
94The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
95Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
96Further, 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).
97
98The 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.
99For 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.
100An open source emulator for the processor, MCU8051 IDE, is also available.
101
102% Processor architecture
103The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
104A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}.
105
106% Internal RAM
107Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
108Internal 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.
109Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7).
110These sit in the first eight bytes of IRAM, though can be programmatically `shifted up' as needed.
111Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks.
112What remains of the IRAM may be treated as general purpose memory.
113
114% External RAM
115External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
116XRAM is accessed using a dedicated instruction.
117External code memory is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
118However, 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).
119
120% ALU
121The 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.
122Further, the processor possesses two eight bit general purpose accumulators, A and B.
123
124% Serial I/O and the input-output lines
125Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
126Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation.
127(The 8052 provides an additional sixteen bit timer.)
128As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
129
130%
131The programmer may take advantage of the interrupt mechanism that the processor provides.
132This 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.
133
134Interrupts 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.
135However, interrupts may be set to one of two priorities: low and high.
136The 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.
137
138The 8051 has interrupts disabled by default.
139The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
140Similarly, `exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags.
141
142\section{The emulator in O'Caml}
143\label{sect.emulator.in.ocaml}
144
145\subsection{Anatomy of the emulator}
146\label{subsect.anatomy.emulator}
147
148We provide a high-level overview of the operation of the emulator.
149
150% Intel HEX, parsing
151Program code is loaded onto the 8051 in a standard format, the Intel Hex (IHX) format.
152All 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.
153Accordingly, our O'Caml emulator can parse IHX files and populate the emulator's code memory with their contents.
154
155Once 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.
156
157\section{The emulator in Matita}
158\label{sect.emulator.in.matita}
159
160\end{document}
Note: See TracBrowser for help on using the repository browser.