Dec 3, 2010, 4:47:48 PM (11 years ago)

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

1 edited


  • Deliverables/D4.1/Report/report.tex

    r348 r371  
     1\documentclass[11pt, epsf, a4wide]{article}
     15\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
     37Report n. D4.1\\
     38Intel 8051/8052 emulator prototype, and formalisation in Matita}
     45Version 1.0
     52Main Authors:\\
     53Claudio Sacerdoti Coen and Dominic P. Mulligan
     60Project Acronym: \cerco{}\\
     61Project full title: Certified Complexity\\
     62Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
     66\markright{\cerco{}, FP7-ICT-2009-C-243881}
     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.
     86\subsection{A brief overview of the target processor}
     90\caption{High level overview of the 8051 memory layout}
     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).
     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.
     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}.
     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.
     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).
     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.
     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.
     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.
     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.
     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.
     142\section{The emulator in O'Caml}
     145\subsection{Anatomy of the emulator}
     148We provide a high-level overview of the operation of the emulator.
     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.
     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.
     157\section{The emulator in Matita}
Note: See TracChangeset for help on using the changeset viewer.