Changeset 574 for Deliverables
- Timestamp:
- Feb 18, 2011, 1:32:46 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r572 r574 66 66 67 67 \begin{abstract} 68 We summarise ourformalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant.68 We summarise the formalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant. 69 69 The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices. 70 70 71 71 The formalisation proceeded in two stages, first implementing an O'Caml prototype, for quickly `ironing out' bugs, and then porting the O'Caml emulator to Matita. 72 72 Though mostly straight-forward, this porting presented multiple problems. 73 Of particular interest is how we handled the unorthoganality of the MSC-51's instruction set.73 Of particular interest is how the unorthoganality of the MSC-51's instruction set is handled. 74 74 In O'Caml, this was handled with polymorphic variants. 75 75 In Matita, we achieved the same effect with a non-standard use of dependent types. … … 140 140 The latter is what we describe in this paper. 141 141 The focus of the formalisation has been on capturing the intensional behaviour of the processor. 142 However, the design of the MCS-51 itself has caused problems in ourformalisation.142 However, the design of the MCS-51 itself has caused problems in the formalisation. 143 143 For example, the MCS-51 has a highly unorthogonal instruction set. 144 144 To cope with this unorthogonality, and to produce an executable specification, we rely on Matita's dependent types. … … 152 152 For instance, the open source Small Device C Compiler (SDCC) recognises a dialect of C~\cite{sdcc:2010}, and other compilers for BASIC, Forth and Modula-2 are also extant. 153 153 An open source emulator for the processor, MCU 8051 IDE, is also available~\cite{mcu8051ide:2010}. 154 Both MCU 8051 IDE and SDCC were used in for validating ourformalisation.154 Both MCU 8051 IDE and SDCC were used in for validating the formalisation. 155 155 156 156 \begin{figure}[t] … … 277 277 \paragraph{Overview of paper}\quad 278 278 In Section~\ref{sect.design.issues.formalisation} we discuss design issues in the development of the formalisation. 279 In Section~\ref{sect.validation} we discuss how we validated the design and implementation of ouremulator to ensure that what we formalised was an accurate model of an MCS-51 series microprocessor.279 In Section~\ref{sect.validation} we discuss how we validated the design and implementation of the emulator to ensure that what we formalised was an accurate model of an MCS-51 series microprocessor. 280 280 In Section~\ref{sect.related.work} we describe previous work, with an eye toward describing its relation with the work described herein. 281 281 In Section~\ref{sect.conclusions} we conclude. … … 296 296 \label{subsect.development.strategy} 297 297 298 Ourimplementation progressed in two stages.298 The implementation progressed in two stages. 299 299 We began with an emulator written in O'Caml to `iron out' any bugs in the design and implementation. 300 300 O'Caml's ability to perform file I/O also eased debugging and validation. … … 340 340 The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits), and also more exoteric quantities (7, 3 and 9-bits). 341 341 To avoid difficult-to-trace size mismatch bugs, we represented all quantities using bitvectors, i.e. fixed length vectors of booleans. 342 In ourO'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}.342 In the 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}. 343 343 From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes. 344 344 However, the module's interface (right column) enforces size invariants in the rest of the code. … … 364 364 365 365 The MCS-51 has numerous disjoint memory spaces addressed by differently sized pointers. 366 In ourO'Caml implementation, we use a map data structure (from the standard library) for each space.366 In the O'Caml implementation, we use a map data structure (from the standard library) for each space. 367 367 Matita's standard library is small, and does not contain a generic map data structure. 368 368 We had the opportunity of crafting a dependently typed special-purpose data structure for the job to enforce the correspondence between the size of pointer and the size of the memory space. … … 370 370 371 371 We picked a modified form of trie of fixed height $h$. 372 Paths are represented by bitvectors (already used in ourimplementation for addresses and registers) of length $h$:372 Paths are represented by bitvectors (already used in the implementation for addresses and registers) of length $h$: 373 373 \begin{lstlisting} 374 374 inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝ … … 405 405 A pseudoinstruction \texttt{Mov} moves (16-bit) data stored at a label into the MCS-51's one 16-bit register, \texttt{DPTR}. 406 406 407 Ourpseudoinstructions and labels induce an assembly language similar to that of SDCC's.407 The pseudoinstructions and labels induce an assembly language similar to that of SDCC's. 408 408 All pseudoinstructions and labels are `assembled away' prior to program execution. 409 409 Jumps are computed in two stages. … … 491 491 ... 492 492 \end{lstlisting} 493 Which were then combined in our inductive datatype for assemblyinstructions using the union operator `$|$':493 Which were then combined in the inductive datatype for assembly preinstructions using the union operator `$|$': 494 494 \begin{lstlisting} 495 495 type 'addr preinstruction = … … 567 567 Proof obligations require us to state and prove a few auxilliary lemmas related to the transitivity of subtyping. 568 568 For instance, an \texttt{addressing\_mode} that belongs to an allowed set also belongs to any one of its supersets. 569 At the moment, Matita's automation exploits these lemmas to completely solve all the proof obligations opened in ourformalisation.569 At the moment, Matita's automation exploits these lemmas to completely solve all the proof obligations opened in the formalisation. 570 570 The \texttt{execute\_1} function, for instance, opens over 200 proof obligations during type checking. 571 571 … … 631 631 We leave the computation of the delay time to the environment. 632 632 633 We use only the P1 and P3 lines despite the MCS-51 having fouroutput lines, P0--P3.633 We use only the P1 and P3 lines despite the MCS-51 having 4 output lines, P0--P3. 634 634 This is because P0 and P2 become inoperable if the processor is equipped with XRAM (we assume it is). 635 635 … … 668 668 Intel HEX is a standard format that all compilers targetting the MCS-51, and similar processors, produce. 669 669 It is essentially a snapshot of the processor's code memory in compressed form. 670 Using this we were able to compile C programs with SDCC and load the resulting program directly into ouremulator's code memory, ready for execution.671 Further, we can produce a HEX file from ouremulator's code memory for loading into third party tools.670 Using this we were able to compile C programs with SDCC and load the resulting program directly into the emulator's code memory, ready for execution. 671 Further, we can produce a HEX file from the emulator's code memory for loading into third party tools. 672 672 After each step of execution, we can print out both the instruction that had been executed and a snapshot of the processor's state, including all flags and register contents. 673 673 For example: … … 696 696 697 697 We further used MCU 8051 IDE as a reference, which allows a user to step through an assembly program one instruction at a time. 698 Using ourexecution traces, we were able to step through a compiled program in MCU 8051 IDE and compare the resulting execution trace with the trace produced by our emulator.699 700 OurMatita formalisation was largely copied from the O'Caml source code, apart from the changes already mentioned.698 Using these execution traces, we were able to step through a compiled program in MCU 8051 IDE and compare the resulting execution trace with the trace produced by our emulator. 699 700 The Matita formalisation was largely copied from the O'Caml source code, apart from the changes already mentioned. 701 701 However, as the Matita emulator is executable, we could perform further validation by comparing the trace of a program's execution in the Matita emulator with the trace of the same program in the O'Caml emulator. 702 702 … … 795 795 796 796 \end{document} 797 798 \newpage799 800 \appendix801 802 \section{Listing of main O'Caml functions}803 \label{sect.listing.main.ocaml.functions}804 805 \subsubsection{From \texttt{ASMInterpret.ml(i)}}806 807 \begin{center}808 \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}809 Name & Description \\810 \hline811 \texttt{assembly} & Assembles an abstract syntax tree representing an 8051 assembly program into a list of bytes, its compiled form. \\812 \texttt{initialize} & Initializes the emulator status. \\813 \texttt{load} & Loads an assembled program into the emulator's code memory. \\814 \texttt{fetch} & Fetches the next instruction, and automatically increments the program counter. \\815 \texttt{execute} & Emulates the processor. Accepts as input a function that pretty prints the emulator status after every emulation loop. \\816 \end{tabular*}817 \end{center}818 819 \subsubsection{From \texttt{ASMCosts.ml(i)}}820 821 \begin{center}822 \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}823 Name & Description \\824 \hline825 \texttt{compute} & Computes a map associating costings to basic blocks in the program.826 \end{tabular*}827 \end{center}828 829 \subsubsection{From \texttt{IntelHex.ml(i)}}830 831 \begin{center}832 \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}833 Name & Description \\834 \hline835 \texttt{intel\_hex\_of\_file} & Reads in a file and parses it if in Intel IHX format, otherwise raises an exception. \\836 \texttt{process\_intel\_hex} & Accepts a parsed Intel IHX file and populates a hashmap (of the same type as code memory) with the contents.837 \end{tabular*}838 \end{center}839 840 \subsubsection{From \texttt{Physical.ml(i)}}841 842 \begin{center}843 \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}844 Name & Description \\845 \hline846 \texttt{subb8\_with\_c} & Performs an eight bit subtraction on bitvectors. The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\847 \texttt{add8\_with\_c} & Performs an eight bit addition on bitvectors. The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\848 \texttt{dec} & Decrements an eight bit bitvector with underflow, if necessary. \\849 \texttt{inc} & Increments an eight bit bitvector with overflow, if necessary.850 \end{tabular*}851 \end{center}852 853 \newpage854 855 \section{Listing of main Matita functions}856 \label{sect.listing.main.matita.functions}857 858 \subsubsection{From \texttt{Arithmetic.ma}}859 860 \begin{center}861 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}862 Title & Description \\863 \hline864 \texttt{add\_n\_with\_carry} & Performs an $n$ bit addition on bitvectors. The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\865 \texttt{sub\_8\_with\_carry} & Performs an eight bit subtraction on bitvectors. The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\866 \texttt{half\_add} & Performs a standard half addition on bitvectors, returning the result and carry bit. \\867 \texttt{full\_add} & Performs a standard full addition on bitvectors and a carry bit, returning the result and a carry bit.868 \end{tabular*}869 \end{center}870 871 \subsubsection{From \texttt{Assembly.ma}}872 873 \begin{center}874 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}875 Title & Description \\876 \hline877 \texttt{assemble1} & Assembles a single 8051 assembly instruction into its memory representation. \\878 \texttt{assemble} & Assembles an 8051 assembly program into its memory representation.\\879 \texttt{assemble\_unlabelled\_program} &\\& Assembles a list of (unlabelled) 8051 assembly instructions into its memory representation.880 \end{tabular*}881 \end{center}882 883 \subsubsection{From \texttt{BitVectorTrie.ma}}884 885 \begin{center}886 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}887 Title & Description \\888 \hline889 \texttt{lookup} & Returns the data stored at the end of a particular path (a bitvector) from the trie. If no data exists, returns a default value. \\890 \texttt{insert} & Inserts data into a tree at the end of the path (a bitvector) indicated. Automatically expands the tree (by filling in stubs) if necessary.891 \end{tabular*}892 \end{center}893 894 \subsubsection{From \texttt{DoTest.ma}}895 896 \begin{center}897 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}898 Title & Description \\899 \hline900 \texttt{execute\_trace} & Executes an assembly program for a fixed number of steps, recording in a trace which instructions were executed.901 \end{tabular*}902 \end{center}903 904 \subsubsection{From \texttt{Fetch.ma}}905 906 \begin{center}907 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}908 Title & Description \\909 \hline910 \texttt{fetch} & Decodes and returns the instruction currently pointed to by the program counter and automatically increments the program counter the required amount to point to the next instruction. \\911 \end{tabular*}912 \end{center}913 914 \subsubsection{From \texttt{Interpret.ma}}915 916 \begin{center}917 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}918 Title & Description \\919 \hline920 \texttt{execute\_1} & Executes a single step of an 8051 assembly program. \\921 \texttt{execute} & Executes a fixed number of steps of an 8051 assembly program.922 \end{tabular*}923 \end{center}924 925 \subsubsection{From \texttt{Status.ma}}926 927 \begin{center}928 \begin{tabular*}{\textwidth}{p{3cm}p{9cm}}929 Title & Description \\930 \hline931 \texttt{load} & Loads an assembled 8051 assembly program into code memory.932 \end{tabular*}933 \end{center}934 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.