Changeset 371

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

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

File:
1 edited

Legend:

Unmodified
 r348 \documentclass[11pt, epsf, a4wide]{article} \usepackage{../../style/cerco} \usepackage{amsfonts} \usepackage{amsmath} \usepackage{amssymb} \usepackage[english]{babel} \usepackage{url} \title{ INFORMATION AND COMMUNICATION TECHNOLOGIES\\ (ICT)\\ PROGRAMME\\ \vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}} \date{} \author{} \begin{document} \thispagestyle{empty} \vspace*{-1cm} \begin{center} \includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png} \end{center} \begin{minipage}{\textwidth} \maketitle \end{minipage} \vspace*{0.5cm} \begin{center} \begin{LARGE} \textbf{ Report n. D4.1\\ Intel 8051/8052 emulator prototype, and formalisation in Matita} \end{LARGE} \end{center} \vspace*{2cm} \begin{center} \begin{large} Version 1.0 \end{large} \end{center} \vspace*{0.5cm} \begin{center} \begin{large} Main Authors:\\ Claudio Sacerdoti Coen and Dominic P. Mulligan \end{large} \end{center} \vspace*{\fill} \noindent Project Acronym: \cerco{}\\ Project full title: Certified Complexity\\ Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\ \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881} \newpage \vspace*{7cm} \paragraph{Abstract} We 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. \newpage \tableofcontents \newpage \section{Introduction} \label{sect.introduction} \subsection{Task} \label{subsect.task} \subsection{A brief overview of the target processor} \label{subsect.brief.overview.target.processor} \begin{figure} \caption{High level overview of the 8051 memory layout} \label{fig.memory.layout} \end{figure} The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s. Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers. Further, 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). The 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. For 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. An open source emulator for the processor, MCU8051 IDE, is also available. % Processor architecture The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation. A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}. % Internal RAM Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory. Internal 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. Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7). These sit in the first eight bytes of IRAM, though can be programmatically shifted up' as needed. Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks. What remains of the IRAM may be treated as general purpose memory. % External RAM External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer. XRAM is accessed using a dedicated instruction. External code memory is often stored in the form of an EPROM, and limited to 64 kilobytes in size. However, 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). % ALU The 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. Further, the processor possesses two eight bit general purpose accumulators, A and B. % Serial I/O and the input-output lines Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes. Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation. (The 8052 provides an additional sixteen bit timer.) As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port. % The programmer may take advantage of the interrupt mechanism that the processor provides. This 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. Interrupts 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. However, interrupts may be set to one of two priorities: low and high. The 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. The 8051 has interrupts disabled by default. The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs. Similarly, exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags. \section{The emulator in O'Caml} \label{sect.emulator.in.ocaml} \subsection{Anatomy of the emulator} \label{subsect.anatomy.emulator} We provide a high-level overview of the operation of the emulator. % Intel HEX, parsing Program code is loaded onto the 8051 in a standard format, the Intel Hex (IHX) format. All 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. Accordingly, our O'Caml emulator can parse IHX files and populate the emulator's code memory with their contents. Once 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. \section{The emulator in Matita} \label{sect.emulator.in.matita} \end{document}