# Changeset 511

Ignore:
Timestamp:
Feb 14, 2011, 5:30:17 PM (6 years ago)
Message:

validation section complete

File:
1 edited

### Legend:

Unmodified
 r510 \usepackage[english]{babel} \usepackage{color} \usepackage{fancybox} \usepackage{graphicx} \usepackage[utf8x]{inputenc} \usepackage{stmaryrd} \usepackage{url} \newlength{\mylength} \newenvironment{frametxt}% {\setlength{\fboxsep}{5pt} \setlength{\mylength}{\linewidth}% \addtolength{\mylength}{-2\fboxsep}% \addtolength{\mylength}{-2\fboxrule}% \Sbox \minipage{\mylength}% \setlength{\abovedisplayskip}{0pt}% \setlength{\belowdisplayskip}{0pt}% }% {\endminipage\endSbox $\fbox{\TheSbox}$} \lstdefinelanguage{matita-ocaml} % SECTION                                                                      % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Representing memory} \label{subsect.representing.memory} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % SECTION                                                                      % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Putting dependent types to work} \label{subsect.putting.dependent.types.to.work} \label{sect.validation} We spent considerable effort attempting to ensure that our formalisation is correct, that is, what we have formalised really is an accurate model of the MCS-51 microprocessor. First, we made use of multiple data sheets, each from a different semiconductor manufacturer. This helped us spot errors in the specification of the processor's instruction set, and its behaviour. The O'Caml prototype was especially useful for validation purposes. This is because we wrote a module for parsing and loading the Intel HEX file format. HEX is a standard format that all compilers targetting the MCS-51, and similar processors, produce. It is essentially a snapshot of the processor's code memory in compressed form. Using this, we were able to compile C programs with SDCC, an open source compiler, and load the resulting program directly into our emulator's code memory, ready for execution. Further, we are able to produce a HEX file from our emulator's code memory, for loading into third party tools. After each step of execution, we can print out both the instruction that had been executed, along with its arguments, and a snapshot of the processor's state, including all flags and register contents. For example: \begin{frametxt} \begin{verbatim} ... 08: mov 81 #07 Processor status: ACC : 0 (00000000) B   : 0 (00000000) PSW : 0 (00000000) with flags set as: CY  : false   AC  : false FO  : false   RS1 : false RS0 : false   OV  : false UD  : false   P   : false SP  : 7 (00000111) IP  : 0 (00000000) PC  : 8 (0000000000001000) DPL : 0 (00000000) DPH : 0 (00000000) SCON: 0 (00000000) SBUF: 0 (00000000) TMOD: 0 (00000000) TCON: 0 (00000000) Registers: R0 : 0 (00000000) R1 : 0 (00000000) R2 : 0 (00000000) R3 : 0 (00000000) R4 : 0 (00000000) R5 : 0 (00000000) R6 : 0 (00000000) R7 : 0 (00000000) ... \end{verbatim} \end{frametxt} Here, the traces indicates that the instruction \texttt{mov 81 \#07} has just been executed by the processor, which is now in the state indicated. These traces were useful in spotting anything that was `obviously' wrong with the execution of the program. Further, we made use of an open source emulator for the MCS-51, \texttt{mcu8051ide}. Using our execution traces, we were able to step through a compiled program, one instruction at a time, in \texttt{mcu8051ide}, and compare the resulting execution trace with the trace produced by our emulator. Our Matita formalisation was largely copied from the O'Caml source code, apart from changes related to addressing modes already mentioned. 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. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % SECTION                                                                      %