Changeset 536
- Timestamp:
- Feb 16, 2011, 4:29:30 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r532 r536 248 248 249 249 \begin{figure}[t] 250 \begin{minipage}[t]{0. 5\textwidth}250 \begin{minipage}[t]{0.45\textwidth} 251 251 \vspace{0pt} 252 252 \begin{lstlisting} … … 254 254 type word = [`Sixteen] vect 255 255 type byte = [`Eight] vect 256 letfrom_nibble =256 $\color{blue}{\mathtt{let}}$ from_nibble = 257 257 function 258 [b1; b2; b3;b4] -> b1,b2,b3,b4258 [b1;b2;b3;b4] -> b1,b2,b3,b4 259 259 | _ -> assert false 260 260 \end{lstlisting} 261 261 \end{minipage} 262 \quad 263 \begin{minipage}[t]{0.5 \textwidth}262 % 263 \begin{minipage}[t]{0.55\textwidth} 264 264 \vspace{0pt} 265 265 \begin{lstlisting} … … 298 298 \label{subsect.representing.memory} 299 299 300 % Different memory spaces are addressed with different sized pointers, and may use different addressing modes301 % 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 cases304 305 300 The MCS-51 has numerous different types of memory. 306 301 In our prototype implementation, we simply used a map datastructure from the O'Caml standard library. 307 302 Matita'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. s303 Therefore, we had the opportunity of crafting a special-purpose datastructure for the job. 309 304 310 305 We worked under the assumption that large swathes of memory would often be uninitialized. … … 377 372 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. 378 373 374 Here, it appears that the MCS-51's memory spaces are completely disjoint. 375 This is not so; many of them overlap with each other, and there's a many-many relationship between addressing modes and memory spaces. 376 For instance, \texttt{DIRECT} addressing can be used to address low internal RAM and the SFRs, but not high internal RAM. 377 378 For simplicity, we merely treat memory spaces as if they are completely disjoint in the \texttt{Status} record. 379 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. 380 379 381 Both 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 382 382 The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}. 383 383 An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned. … … 550 550 The processor then executes the instruction, followed by the code implementing the timers. 551 551 552 % Discuss I/O 552 I/O is handled with a continuation: 553 \begin{lstlisting} 554 type line = 555 [ `P1 of byte | `P3 of byte 556 | `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]] 557 type continuation = 558 [`In of time * line * epsilon * continuation] option * 559 [`Out of (time -> line -> time * continuation)] 560 \end{lstlisting} 561 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. 562 Input and output are handled with \texttt{continuation}, 553 563 554 564 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset
for help on using the changeset viewer.