# Changeset 536 for Deliverables/D4.1/ITP-Paper/itp-2011.tex

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

 r532 \begin{figure}[t] \begin{minipage}[t]{0.5\textwidth} \begin{minipage}[t]{0.45\textwidth} \vspace{0pt} \begin{lstlisting} type word = [Sixteen] vect type byte = [Eight] vect let from_nibble = $\color{blue}{\mathtt{let}}$ from_nibble = function [b1; b2; b3; b4] -> b1,b2,b3,b4 [b1;b2;b3;b4] -> b1,b2,b3,b4 | _ -> assert false \end{lstlisting} \end{minipage} \quad \begin{minipage}[t]{0.5\textwidth} % \begin{minipage}[t]{0.55\textwidth} \vspace{0pt} \begin{lstlisting} \label{subsect.representing.memory} % Different memory spaces are addressed with different sized pointers, and may use different addressing modes % Many-many map between addressing modes and memory spaces (e.g. DIRECT can be used to address low internal RAM and SFRs) % Maybe show snippet of get/set_arg_8? % Discuss overlapping memory: we implement as if disjoint memory spaces, but when we get/set we handle overlapping cases The MCS-51 has numerous different types of memory. In our prototype implementation, we simply used a map datastructure from the O'Caml standard library. Matita's standard library is relatively small, and does not contain a generic map datastructure. Therefore, we had the opportunity of crafting a special-purpose datastructure for the job.s Therefore, we had the opportunity of crafting a special-purpose datastructure for the job. We worked under the assumption that large swathes of memory would often be uninitialized. This 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. Here, it appears that the MCS-51's memory spaces are completely disjoint. This is not so; many of them overlap with each other, and there's a many-many relationship between addressing modes and memory spaces. For instance, \texttt{DIRECT} addressing can be used to address low internal RAM and the SFRs, but not high internal RAM. For simplicity, we merely treat memory spaces as if they are completely disjoint in the \texttt{Status} record. Overlapping, 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. Both the Matita and O'Caml emulators follows the classic fetch-decode-execute' model of processor operation. The most important functions in the Matita emulator are highlighted below. The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}. An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned. The processor then executes the instruction, followed by the code implementing the timers. % Discuss I/O I/O is handled with a continuation: \begin{lstlisting} type line = [ P1 of byte | P3 of byte | SerialBuff of [ Eight of byte | Nine of BitVectors.bit * byte ]] type continuation = [In of time * line * epsilon * continuation] option * [Out of (time -> line -> time * continuation)] \end{lstlisting} The \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. Input and output are handled with \texttt{continuation}, %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%