Changeset 371


Ignore:
Timestamp:
Dec 3, 2010, 4:47:48 PM (9 years ago)
Author:
mulligan
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Report/report.tex

    r348 r371  
     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 TracChangeset for help on using the changeset viewer.