Changeset 536


Ignore:
Timestamp:
Feb 16, 2011, 4:29:30 PM (6 years ago)
Author:
mulligan
Message:

more added

File:
1 edited

Legend:

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

    r532 r536  
    248248
    249249\begin{figure}[t]
    250 \begin{minipage}[t]{0.5\textwidth}
     250\begin{minipage}[t]{0.45\textwidth}
    251251\vspace{0pt}
    252252\begin{lstlisting}
     
    254254type word = [`Sixteen] vect
    255255type byte = [`Eight] vect
    256 let from_nibble =
     256$\color{blue}{\mathtt{let}}$ from_nibble =
    257257 function
    258     [b1; b2; b3; b4] -> b1,b2,b3,b4
     258    [b1;b2;b3;b4] -> b1,b2,b3,b4
    259259  | _ -> assert false
    260260\end{lstlisting}
    261261\end{minipage}
    262 \quad
    263 \begin{minipage}[t]{0.5\textwidth}
     262%
     263\begin{minipage}[t]{0.55\textwidth}
    264264\vspace{0pt}
    265265\begin{lstlisting}
     
    298298\label{subsect.representing.memory}
    299299
    300 % Different memory spaces are addressed with different sized pointers, and may use different addressing modes
    301 % Many-many map between addressing modes and memory spaces (e.g. DIRECT can be used to address low internal RAM and SFRs)
    302 % Maybe show snippet of get/set_arg_8?
    303 % Discuss overlapping memory: we implement as if disjoint memory spaces, but when we get/set we handle overlapping cases
    304 
    305300The MCS-51 has numerous different types of memory.
    306301In our prototype implementation, we simply used a map datastructure from the O'Caml standard library.
    307302Matita's standard library is relatively small, and does not contain a generic map datastructure.
    308 Therefore, we had the opportunity of crafting a special-purpose datastructure for the job.s
     303Therefore, we had the opportunity of crafting a special-purpose datastructure for the job.
    309304
    310305We worked under the assumption that large swathes of memory would often be uninitialized.
     
    377372This was due to a bug in Matita when we were constructing the emulator, since fixed, where the time needed to typecheck a record grew exponentially with the number of fields.
    378373
     374Here, it appears that the MCS-51's memory spaces are completely disjoint.
     375This is not so; many of them overlap with each other, and there's a many-many relationship between addressing modes and memory spaces.
     376For instance, \texttt{DIRECT} addressing can be used to address low internal RAM and the SFRs, but not high internal RAM.
     377
     378For simplicity, we merely treat memory spaces as if they are completely disjoint in the \texttt{Status} record.
     379Overlapping, and checking which addressing modes can be used to address particular memory spaces, is handled through numerous \texttt{get\_arg\_XX} and \texttt{set\_arg\_XX} (for 1, 8 and 16 bits) functions.
     380
    379381Both the Matita and O'Caml emulators follows the classic `fetch-decode-execute' model of processor operation.
    380 The most important functions in the Matita emulator are highlighted below.
    381 
    382382The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
    383383An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned.
     
    550550The processor then executes the instruction, followed by the code implementing the timers.
    551551
    552 % Discuss I/O
     552I/O is handled with a continuation:
     553\begin{lstlisting}
     554type line =
     555  [ `P1 of byte | `P3 of byte
     556  | `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]]
     557type continuation =
     558  [`In of time * line * epsilon * continuation] option *
     559  [`Out of (time -> line -> time * continuation)]
     560\end{lstlisting}
     561The \texttt{line} datatype signals which input/output channel is being used, either the P1 or P3 lines, or the UART port in eight or nine bit mode.
     562Input and output are handled with \texttt{continuation},
    553563
    554564%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.