Changeset 808
 Timestamp:
 May 16, 2011, 10:44:06 AM (10 years ago)
 Location:
 Deliverables/D4.1/ITPPaper
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.tex
r580 r808 1 \documentclass {llncs}1 \documentclass[10pt, final, conference]{IEEEtran} 2 2 3 3 \usepackage{amsfonts} … … 37 37 } 38 38 \lstset{language=matitaocaml,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}, 44 44 showspaces=false,showstringspaces=false} 45 \lstset{extendedchars=false}46 \lstset{inputencoding=utf8x}47 45 \DeclareUnicodeCharacter{8797}{:=} 48 46 \DeclareUnicodeCharacter{10746}{++} … … 50 48 \DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} 51 49 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 MCS51 microprocessor in Matita} 65 66 \thanks{The project CerCo acknowledges the financial support of the Future and 53 67 Emerging Technologies (FET) programme within the Seventh Framework 54 68 Programme for Research of the European Commission, under FETOpen 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 MCS51 microprocessor in Matita} 58 \titlerunning{An executable formalisation of the MCS51} 59 \institute{Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna} 69 number: 243881} 60 70 61 71 \bibliographystyle{plain} … … 79 89 The formalisation is a major component of the ongoing EUfunded CerCo project. 80 90 \end{abstract} 91 92 \begin{IEEEkeywords} 93 Hardware formalisation, Matita, dependent types, CerCo 94 \end{IEEEkeywords} 81 95 82 96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% … … 154 168 Both MCU 8051 IDE and SDCC were used in for validating the formalisation. 155 169 156 \begin{figure}[t] 170 \begin{figure*} 171 \centering 157 172 \setlength{\unitlength}{0.87pt} 158 173 \begin{picture}(410,250)(50,200) … … 224 239 \caption{The 8051 memory model} 225 240 \label{fig.memory.layout} 226 \end{figure }241 \end{figure*} 227 242 228 243 The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation. … … 316 331 \begin{minipage}[t]{0.45\textwidth} 317 332 \vspace{0pt} 333 \small{ 318 334 \begin{lstlisting} 319 335 type 'a vect = bit list … … 322 338 $\color{blue}{\mathtt{let}}$ split_word w = split_nth 4 w 323 339 $\color{blue}{\mathtt{let}}$ split_byte b = split_nth 2 b 324 \end{lstlisting} 340 \end{lstlisting}} 325 341 \end{minipage} 326 342 % … … 510 526 Here, \texttt{union6} is a disjoint union type, defined as follows: 511 527 \begin{lstlisting} 512 type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a  ...  `U6 of 'f ] 528 type ('a,'b,'c,'d,'e,'f) union6 = 529 [ `U1 of 'a  ...  `U6 of 'f ] 513 530 \end{lstlisting} 514 531 For our purposes, the types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed. … … 583 600 let status := set_8051_sfr status SFR_DPL bl in 584 601 status 585  _ $\Rightarrow$ $\lambda$_: False. $\bot$ ] $~$(subaddressing_modein $\ldots$ a). 602  _ $\Rightarrow$ $\lambda$_: False. $\bot$ ] 603 $~$(subaddressing_modein $\ldots$ a). 586 604 \end{lstlisting} 587 605 We 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. … … 616 634 type line = 617 635 [ `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 ] 619 640 type continuation = 620 [`In of time * line * epsilon * continuation] option * 641 [`In of time * line * 642 epsilon * continuation] option * 621 643 [`Out of (time > line > time * continuation)] 622 644 \end{lstlisting} … … 675 697 SBUF: 0 TMOD: 0 TCON: 0 676 698 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 678 701 \end{verbatim} 679 702 \end{scriptsize}
Note: See TracChangeset
for help on using the changeset viewer.