Changeset 808 for Deliverables


Ignore:
Timestamp:
May 16, 2011, 10:44:06 AM (9 years ago)
Author:
mulligan
Message:

Changes to paper to get it ready for FMCAD

Location:
Deliverables/D4.1/ITP-Paper
Files:
1 added
1 edited

Legend:

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

    r580 r808  
    1 \documentclass{llncs}
     1\documentclass[10pt, final, conference]{IEEEtran}
    22
    33\usepackage{amsfonts}
     
    3737  }
    3838\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
    39         keywordstyle=\color{red}\bfseries,
    40         keywordstyle=[2]\color{blue},
    41         keywordstyle=[3]\color{blue}\bfseries,
    42         commentstyle=\color{green},
    43         stringstyle=\color{blue},
     39        keywordstyle=\bfseries, %\color{red}\bfseries,
     40        keywordstyle=[2]\bfseries, %\color{blue},
     41        keywordstyle=[3]\bfseries, %\color{blue}\bfseries,
     42%        commentstyle=\color{green},
     43%        stringstyle=\color{blue},
    4444        showspaces=false,showstringspaces=false}
    45 \lstset{extendedchars=false}
    46 \lstset{inputencoding=utf8x}
    4745\DeclareUnicodeCharacter{8797}{:=}
    4846\DeclareUnicodeCharacter{10746}{++}
     
    5048\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
    5149
    52 \author{Dominic P. Mulligan\thanks{The project CerCo acknowledges the financial support of the Future and
     50\lstset{
     51  extendedchars=false,
     52  inputencoding=utf8x,
     53  tabsize=1
     54}
     55
     56\author{
     57  \IEEEauthorblockN{Dominic P. Mulligan}
     58  \IEEEauthorblockA{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
     59\and
     60  \IEEEauthorblockN{Claudio Sacerdoti Coen}
     61  \IEEEauthorblockA{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
     62}
     63
     64\title{An executable formalisation of the MCS-51 microprocessor in Matita}
     65
     66\thanks{The project CerCo acknowledges the financial support of the Future and
    5367Emerging Technologies (FET) programme within the Seventh Framework
    5468Programme for Research of the European Commission, under FET-Open grant
    55 number: 243881} \and Claudio Sacerdoti Coen$^\star$}
    56 \authorrunning{D. P. Mulligan and C. Sacerdoti Coen}
    57 \title{An executable formalisation of the MCS-51 microprocessor in Matita}
    58 \titlerunning{An executable formalisation of the MCS-51}
    59 \institute{Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna}
     69number: 243881}
    6070
    6171\bibliographystyle{plain}
     
    7989The formalisation is a major component of the ongoing EU-funded CerCo project.
    8090\end{abstract}
     91
     92\begin{IEEEkeywords}
     93Hardware formalisation, Matita, dependent types, CerCo
     94\end{IEEEkeywords}
    8195
    8296%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    154168Both MCU 8051 IDE and SDCC were used in for validating the formalisation.
    155169
    156 \begin{figure}[t]
     170\begin{figure*}
     171\centering
    157172\setlength{\unitlength}{0.87pt}
    158173\begin{picture}(410,250)(-50,200)
     
    224239\caption{The 8051 memory model}
    225240\label{fig.memory.layout}
    226 \end{figure}
     241\end{figure*}
    227242
    228243The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
     
    316331\begin{minipage}[t]{0.45\textwidth}
    317332\vspace{0pt}
     333\small{
    318334\begin{lstlisting}
    319335type 'a vect = bit list
     
    322338$\color{blue}{\mathtt{let}}$ split_word w = split_nth 4 w
    323339$\color{blue}{\mathtt{let}}$ split_byte b = split_nth 2 b
    324 \end{lstlisting}
     340\end{lstlisting}}
    325341\end{minipage}
    326342%
     
    510526Here, \texttt{union6} is a disjoint union type, defined as follows:
    511527\begin{lstlisting}
    512 type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a | ... | `U6 of 'f ]
     528type ('a,'b,'c,'d,'e,'f) union6 =
     529  [ `U1 of 'a | ... | `U6 of 'f ]
    513530\end{lstlisting}
    514531For our purposes, the types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed.
     
    583600       let status := set_8051_sfr status SFR_DPL bl in
    584601         status
    585      | _ $\Rightarrow$ $\lambda$_: False. $\bot$ ] $~$(subaddressing_modein $\ldots$ a).
     602     | _ $\Rightarrow$ $\lambda$_: False. $\bot$ ]
     603       $~$(subaddressing_modein $\ldots$ a).
    586604\end{lstlisting}
    587605We give a proof (the expression \texttt{(subaddressing\_modein} $\ldots$ \texttt{a)}) that the argument $a$ is in the set $\llbracket$ \texttt{dptr} $\rrbracket$ to the \texttt{match} expression.
     
    616634type line =
    617635  [ `P1 of byte | `P3 of byte
    618   | `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]]
     636  | `SerialBuff of
     637     [ `Eight of byte
     638     | `Nine of BitVectors.bit * byte ]
     639  ]
    619640type continuation =
    620   [`In of time * line * epsilon * continuation] option *
     641  [`In of time * line *
     642          epsilon * continuation] option *
    621643  [`Out of (time -> line -> time * continuation)]
    622644\end{lstlisting}
     
    675697   SBUF: 0   TMOD: 0   TCON: 0
    676698   Registers:                                   
    677     R0: 0   R1: 0   R2: 0   R3: 0   R4: 0   R5: 0   R6: 0   R7: 0
     699    R0: 0   R1: 0   R2: 0   R3: 0
     700    R4: 0   R5: 0   R6: 0   R7: 0
    678701\end{verbatim}
    679702\end{scriptsize}
Note: See TracChangeset for help on using the changeset viewer.