Changeset 371

Dec 3, 2010, 4:47:48 PM (9 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}
     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\\
     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.
     100An open source emulator for the processor, MCU8051 IDE, is also available.
     102% Processor architecture
     106% Internal RAM
     112What remains of the IRAM may be treated as general purpose memory.
     114% External RAM
     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
     122Further, the processor possesses two eight bit general purpose accumulators, A and B.
     124% Serial I/O and the input-output lines
     127(The 8052 provides an additional sixteen bit timer.)
     131The programmer may take advantage of the interrupt mechanism that the processor provides.
     135However, interrupts may be set to one of two priorities: low and high.
     138The 8051 has interrupts disabled by default.
     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.