# Changeset 516

Ignore:
Timestamp:
Feb 15, 2011, 2:12:45 PM (8 years ago)
Message:

 r515 Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory. Internal memory, commonly provided on the die itself with fast access, is further divided into 128 bytes of internal RAM and numerous Special Function Registers (SFRs) which control the operation of the processor. Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7). Internal RAM (IRAM) is further divided into eight general purpose bit-addressable registers (R0--R7). These sit in the first eight bytes of IRAM, though can be programmatically shifted up' as needed. Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks. Bit memory, followed by a small amount of stack space, resides in the memory space immediately after the register banks. What remains of the IRAM may be treated as general purpose memory. A schematic view of IRAM layout is provided in Figure~\ref{fig.iram.layout}. External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer. XRAM is accessed using a dedicated instruction. External RAM (XRAM), limited to a maximum size of 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer. XRAM is accessed using a dedicated instruction, and requires sixteen bits to address fully. External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size. However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied. % SECTION                                                                      % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Emulator architecture} \label{subsect.emulator.architecture} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % SECTION                                                                      % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{From O'Caml prototype to Matita formalisation} \label{sect.from.o'caml.prototype.matita.formalisation} \subsection{Representing memory} \label{subsect.representing.memory} 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. However, when moving to Matita, we aimed to improve our treatment of memory. We worked under the assumption that large swathes of memory would often be uninitialized. Using a complete binary tree, for instance, would therefore be extremely memory inefficient. Instead, we chose to use a modified form of trie, where paths are represented by bitvectors. As bitvectors were widely used in our implementation already for representing integers, this worked well: \begin{quote} \begin{lstlisting} inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝ Leaf: A $\rightarrow$ BitVectorTrie A 0 | Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n) | Stub: ∀n. BitVectorTrie A n. \end{lstlisting} \end{quote} Here, \texttt{Stub} is a constructor that can appear at any point in our tries. It internalises the notion of uninitialized data'. Performing a lookup in memory is now straight-forward. We merely traverse a path, and if at any point we encounter a \texttt{Stub}, we return a default value\footnote{All manufacturer data sheets that we consulted were silent on the subject of what should be returned if we attempt to access uninitialized memory.  We defaulted to simply returning zero, though our \texttt{lookup} function is parametric in this choice.}. As we are using bitvectors, we may make full use of dependent types and ensure that our bitvector paths are of the same length as the height of the tree. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%