Ignore:
Timestamp:
Feb 18, 2011, 10:10:49 AM (9 years ago)
Author:
mulligan
Message:

Added two missing references, reduced back down to 16 pages by rewording some sentences and gaming bibtex file

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r565 r568  
    7878Both the O'Caml and Matita emulators are `executable'.
    7979Assembly programs may be animated within Matita, producing a trace of instructions executed.
    80 
    81 Our formalisation is a major component of the ongoing EU-funded CerCo project.
     80The formalisation is a major component of the ongoing EU-funded CerCo project.
    8281\end{abstract}
    8382
     
    136135These are still widely used in embedded systems, with the advantage of an easily predictable cost model due to their relative paucity of features.
    137136
    138 We have fully formalised an executable formal semantics of a family of 8 bit Freescale Microprocessors~\cite{oliboni:matita:2008}, and provided a similar executable formal semantics for the MCS-51 microprocessor.
     137We have fully formalised an executable formal semantics of a family of 8-bit Freescale Microprocessors~\cite{oliboni:matita:2008}, and provided a similar executable formal semantics for the MCS-51 microprocessor.
    139138The latter is what we describe in this paper.
    140139The focus of the formalisation has been on capturing the intensional behaviour of the processor.
     
    146145\label{subsect.8051-8052}
    147146
    148 The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
     147The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s.
    149148Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
    150149Further, the processor, its immediate successor the 8052, and many derivatives are still manufactured \emph{en masse} by a host of semiconductor suppliers.
     
    239238
    240239External RAM (XRAM), limited to a maximum size of 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
    241 XRAM is accessed using a dedicated instruction, and requires sixteen bits to address fully.
     240XRAM is accessed using a dedicated instruction, and requires 16 bits to address fully.
    242241External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
    243242However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied.
     
    245244Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
    246245As 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.
    247 For 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. Moreover, some memory segments are addressed using 8 bits pointers while others require 16 bits.
    248 
    249 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.
    250 Further, the processor possesses two eight bit general purpose accumulators, A and B.
     246For 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. Moreover, some memory segments are addressed using 8-bit pointers while others require 16-bits.
     247
     248The 8051 possesses an 8-bit Arithmetic and Logic Unit (ALU), with a variety of instructions for performing arithmetic and logical operations on bits and integers.
     249Two 8-bit general purpose accumulators, A and B, are provided.
    251250
    252251Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
    253 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.
    254 (The 8052 provides an additional sixteen bit timer.)
     252Serial baud rate is determined by one of two 16-bit timers included with the 8051, which can be set to multiple modes of operation.
     253(The 8052 provides an additional 16-bit timer.)
    255254As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
    256255
     
    303302We began with an emulator written in O'Caml to `iron out' any bugs in our design and implementation.
    304303O'Caml's ability to perform file I/O also eased debugging and validation.
    305 Once we were happy with the performance and design of the O'Caml emulator, we moved to the Matita formalisation.
     304Once we were happy with the design of the O'Caml emulator, we moved Matita.
    306305
    307306Matita's syntax is lexically similar to O'Caml's.
     
    342341\end{figure}
    343342
    344 The formalization of MCS-51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits).
     343The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits) but also with more exoteric quantities (7-bits, 3-bits, 9-bits).
    345344To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
    346345In our O'Caml emulator, we `faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
     
    483482
    484483A peculiarity of the MCS-51 is the non-orthogonality of its instruction set.
    485 For instance, the \texttt{MOV} instruction, can be invoked using one of sixteen combinations of addressing modes out of 361.
     484For instance, the \texttt{MOV} instruction, can be invoked using one of 16 combinations of addressing modes out of a possible 361.
    486485
    487486% Show example of pattern matching with polymorphic variants
     
    564563...
    565564\end{lstlisting}
    566 We see that the constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), and the second being one of a register, direct, indirect or data addressing mode.
     565The constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), the second being a register, direct, indirect or data addressing mode.
    567566
    568567% One of these coercions opens up a proof obligation which needs discussing
     
    570569The final, missing component is a pair of type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{subaddressing\_mode} to \texttt{Type$\lbrack0\rbrack$}, respectively.
    571570The first is a forgetful coercion, while the second opens a proof obligation wherein we must prove that the provided value is in the admissible set.
    572 These coercions were first introduced by PVS to implement subset types~\cite{pvs?}, and later in Coq as an addition~\cite{russell}.
     571These coercions were first introduced by PVS to implement subset types~\cite{shankar:principles:1999}, and later in Coq as an addition~\cite{sozeau:subset:2006}.
    573572In Matita all coercions can open proof obligations.
    574573
     
    645644
    646645The UART port can work in several modes, depending on the how the SFRs are set.
    647 In an asyncrhonous mode, the UART transmits eight bits at a time, using a ninth line for syncrhonization.
     646In an asyncrhonous mode, the UART transmits 8 bits at a time, using a ninth line for syncrhonization.
    648647In a syncrhonous mode the ninth line is used to transmit an additional bit.
    649648
Note: See TracChangeset for help on using the changeset viewer.