Changeset 524
- Timestamp:
- Feb 15, 2011, 5:26:53 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r523 r524 315 315 % SECTION % 316 316 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 317 \subsection{ Emulator architecture}318 \label{subsect. emulator.architecture}317 \subsection{Anatomy of the (Matita) emulator} 318 \label{subsect.anatomy.matita.emulator} 319 319 320 320 The internal state of our Matita emulator is represented as a record: … … 337 337 One peculiarity is the packing of the 24 combined SFRs into fixed length vectors. 338 338 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. 339 340 Both the Matita and O'Caml emulators follows the classic `fetch-decode-execute' model of processor operation. 341 The most important functions in the Matita emulator are highlighted below. 342 \begin{quote} 343 \begin{lstlisting} 344 definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat := ... 345 \end{lstlisting} 346 \end{quote} 347 The next instruction, indexed by the program counter, is fetched from code memory with \texttt{fetch}. 348 An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned. 349 These costs are taken from a Siemen's data sheet for the MCS-51, and will likely vary across manufacturers and particular derivatives of the processor. 350 \begin{quote} 351 \begin{lstlisting} 352 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ... 353 \end{lstlisting} 354 \end{quote} 355 A single instruction is assembled into its corresponding bit encoding with \texttt{assembly1}: 356 \begin{quote} 357 \begin{lstlisting} 358 definition assembly1: instruction $\rightarrow$ list Byte := ... 359 \end{lstlisting} 360 \end{quote} 361 An assembly program, consisting of a preamble containing global data, and a list of (pseudo)instructions, is assembled using \texttt{assembly}. 362 Pseudoinstructions and labels are eliminated in favour of concrete instructions from the MCS-51 instruction set. 363 A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is also produced. 364 \begin{quote} 365 \begin{lstlisting} 366 definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ... 367 \end{lstlisting} 368 \end{quote} 369 A single execution step of the processor is evaluated using \texttt{execute\_1}, mapping a \texttt{Status} to a \texttt{Status}: 370 \begin{quote} 371 \begin{lstlisting} 372 definition execute_1: Status → Status := ... 373 \end{lstlisting} 374 \end{quote} 375 Multiple steps of processor execution are implemented in \texttt{execute}, which wraps \texttt{execute\_1}: 376 \begin{quote} 377 \begin{lstlisting} 378 let rec execute (n: nat) (s: Status) on n: Status := ... 379 \end{lstlisting} 380 \end{quote} 339 381 340 382 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset
for help on using the changeset viewer.