source:Deliverables/D4.1/ITP-Paper/itp-2011.tex@493

Last change on this file since 493 was 493, checked in by mulligan, 8 years ago

incorporated some text from the eu report that needs to be pared down

File size: 8.7 KB
Line
1\documentclass{llncs}
2
3\usepackage[english]{babel}
4\usepackage{graphicx}
5
6\author{Claudio Sacerdoti Coen \and Dominic P. Mulligan}
7\authorrunning{C. Sacerdoti Coen and D. P. Mulligan}
8\title{An executable model of the 8051/8052 series microprocessor in Matita}
9\titlerunning{An executable model of the 8051/8052}
10\institute{Dipartimento di Scienze dell'Informazione, University of Bologna}
11
12\begin{document}
13
14\maketitle
15
16\begin{abstract}
17We summary the recent encoding of an executable formal model of the 8051/8052 microprocessor within Matita's internal logic.
18\end{abstract}
19
20%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21% SECTION                                                                      %
22%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
23\section{Introduction}
24\label{sect.introduction}
25
26Compiler verification, as of late, is a hot topic' in computer science research.
27This rapidly growing field is motivated by one simple question: to what extent can you trust your compiler?'
28
29\subsection{The 8051/8052}
30\label{subsect.8051-8052}
31
32The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
33Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
34Further, 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).
35
36The 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.
37For 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.
38An open source emulator for the processor, MCU8051 IDE, is also available.
39
40\begin{figure}[t]
41\begin{center}
42\includegraphics[scale=0.5]{memorylayout.png}
43\end{center}
44\caption{High level overview of the 8051 memory layout}
45\label{fig.memory.layout}
46\end{figure}
47
48The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
49A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}.
50
51Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
52Internal 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.
53Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7).
54These sit in the first eight bytes of IRAM, though can be programmatically shifted up' as needed.
55Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks.
56What remains of the IRAM may be treated as general purpose memory.
57A schematic view of IRAM layout is provided in Figure~\ref{fig.iram.layout}.
58
59External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
60XRAM is accessed using a dedicated instruction.
61External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
62However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied.
63
64Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
65As the latter two addressing modes hint, there are some restrictions enforced by the 8051 and its derivatives on which addressing modes may be used with specific types of memory.
66For instance, the 128 bytes of extra internal RAM that the 8052 features cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used.
67
68The 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.
69Further, the processor possesses two eight bit general purpose accumulators, A and B.
70
71Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
72Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation.
73(The 8052 provides an additional sixteen bit timer.)
74As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
75
76The programmer may take advantage of the interrupt mechanism that the processor provides.
77This 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.
78
79Interrupts 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.
80However, interrupts may be set to one of two priorities: low and high.
81The 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.
82
83The 8051 has interrupts disabled by default.
84The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
85Similarly, exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags.
86
87\begin{figure}[t]
88\begin{center}
89\includegraphics[scale=0.5]{iramlayout.png}
90\end{center}
91\caption{Schematic view of 8051 IRAM layout}
92\label{fig.iram.layout}
93\end{figure}
94
95%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
96% SECTION                                                                      %
97%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
98\subsection{The CerCo project}
99\label{subsect.cerco.project}
100
101The CerCo project (`Certified Complexity') is a current European FeT-Open project incorporating three sites---the Universities of Bologna, Edinburgh and Paris Diderot 7---throughout the European Union.
102The ultimate aim of the project is to produce a certified compiler for a large subset of the C programming language targetting a microprocessor used in embedded systems.
103In this respect, the CerCo project bears a deal of similarity with CompCert, another European funded project.
104However, we see a number of important differences between the aims of the two projects.
105\begin{enumerate}
106\item
107The CerCo project aims to allow reasoning on aspects of the intensional properties of C programs.
108That is,
109\item
110The CompCert project compiled a subset of C down to the assembly level.
111A semantics for assembly language was provided.
112\end{enumerate}
113
114%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
115% SECTION                                                                      %
116%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
117\subsection{Overview of paper}
118\label{subsect.overview.paper}
119
120%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
121% SECTION                                                                      %
122%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
123\section{Development strategy}
124\label{sect.development.strategy}
125
126%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
127% SECTION                                                                      %
128%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
129\section{Putting dependent types to work}
130\label{sect.putting.dependent.types.to.work}
131
132%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
133% SECTION                                                                      %
134%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
135\section{Related work}
136\label{sect.related.work}
137
138%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
139% SECTION                                                                      %
140%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
141\section{Conclusions}
142\label{sect.conclusions}
143
144\end{document}
Note: See TracBrowser for help on using the repository browser.