Changeset 511


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

validation section complete

File:
1 edited

Legend:

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

    r510 r511  
    66\usepackage[english]{babel}
    77\usepackage{color}
     8\usepackage{fancybox}
    89\usepackage{graphicx}
    910\usepackage[utf8x]{inputenc}
     
    1213\usepackage{stmaryrd}
    1314\usepackage{url}
     15
     16\newlength{\mylength}
     17\newenvironment{frametxt}%
     18        {\setlength{\fboxsep}{5pt}
     19                \setlength{\mylength}{\linewidth}%
     20                \addtolength{\mylength}{-2\fboxsep}%
     21                \addtolength{\mylength}{-2\fboxrule}%
     22                \Sbox
     23                \minipage{\mylength}%
     24                        \setlength{\abovedisplayskip}{0pt}%
     25                        \setlength{\belowdisplayskip}{0pt}%
     26                }%
     27                {\endminipage\endSbox
     28                        \[\fbox{\TheSbox}\]}
    1429
    1530\lstdefinelanguage{matita-ocaml}
     
    273288% SECTION                                                                      %
    274289%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     290\subsection{Representing memory}
     291\label{subsect.representing.memory}
     292
     293%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     294% SECTION                                                                      %
     295%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    275296\subsection{Putting dependent types to work}
    276297\label{subsect.putting.dependent.types.to.work}
     
    411432\label{sect.validation}
    412433
     434We 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.
     435
     436First, we made use of multiple data sheets, each from a different semiconductor manufacturer.
     437This helped us spot errors in the specification of the processor's instruction set, and its behaviour.
     438
     439The O'Caml prototype was especially useful for validation purposes.
     440This is because we wrote a module for parsing and loading the Intel HEX file format.
     441HEX is a standard format that all compilers targetting the MCS-51, and similar processors, produce.
     442It is essentially a snapshot of the processor's code memory in compressed form.
     443Using 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.
     444Further, we are able to produce a HEX file from our emulator's code memory, for loading into third party tools.
     445After 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.
     446For example:
     447\begin{frametxt}
     448\begin{verbatim}
     449...
     450
     45108: mov 81 #07
     452
     453 Processor status:                               
     454
     455   ACC : 0 (00000000) B   : 0 (00000000)
     456   PSW : 0 (00000000) with flags set as:
     457     CY  : false   AC  : false
     458     FO  : false   RS1 : false
     459     RS0 : false   OV  : false
     460     UD  : false   P   : false
     461   SP  : 7 (00000111) IP  : 0 (00000000)
     462   PC  : 8 (0000000000001000)
     463   DPL : 0 (00000000) DPH : 0 (00000000)
     464   SCON: 0 (00000000) SBUF: 0 (00000000)
     465   TMOD: 0 (00000000) TCON: 0 (00000000)
     466   Registers:                                   
     467    R0 : 0 (00000000) R1 : 0 (00000000)
     468    R2 : 0 (00000000) R3 : 0 (00000000)
     469    R4 : 0 (00000000) R5 : 0 (00000000)
     470    R6 : 0 (00000000) R7 : 0 (00000000)
     471
     472...
     473\end{verbatim}
     474\end{frametxt}
     475Here, the traces indicates that the instruction \texttt{mov 81 \#07} has just been executed by the processor, which is now in the state indicated.
     476These traces were useful in spotting anything that was `obviously' wrong with the execution of the program.
     477
     478Further, we made use of an open source emulator for the MCS-51, \texttt{mcu8051ide}.
     479Using 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.
     480
     481Our Matita formalisation was largely copied from the O'Caml source code, apart from changes related to addressing modes already mentioned.
     482However, 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.
     483
    413484%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    414485% SECTION                                                                      %
Note: See TracChangeset for help on using the changeset viewer.