Changeset 377 for Deliverables
- Timestamp:
- Dec 6, 2010, 11:44:23 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Report/report.tex
r376 r377 177 177 Once code memory is populated, and the rest of the emulator state has been initialised (i.e. setting the program counter to zero), the O'Caml emulator fetches the instruction pointed to by the program counter from code memory. 178 178 179 \subsection{Lack of orthogonality in instruction set} 180 \label{subsect.lack.orthogonality.instruction.set} 181 182 \subsection{Pseudo-instructions} 183 \label{subsect.pseudo-instructions} 184 185 In validating the design and implementation of the O'Caml emulator we used two tactics: 186 \begin{enumerate} 187 \item 188 Use of multiple manufacturer's data sheets (both the Siemens Semiconductor and Phillips Semiconductor specifications for the 8051, as well as online sources such as the Keil website). 189 We found typographic errors in manufacturer's data sheets which were resolved by consulting an alternative sheet. 190 \item 191 Use of reference compilers and emulators. 192 The operation of the emulator was manually tested by reference to \textsc{mcu 8051 ide}, an emulator for the 8051 series processor. 193 A number of small C programs were compiled in SDCC\footnote{See the \texttt{GCC} directory for a selection of them.}, and the resulting IHX files were disassembled by \textsc{mcu 8051 ide}. 194 The status changes in both emulators were then compared. 195 196 For further validation, the output of the compiled C programs from SDCC was compared with the output of the same programs in GCC, in order to pre-empt the introduction of bugs in the emulator inherited from a faulty C compiler. 197 \end{enumerate} 198 199 As a further check, the design and operation of the emulator was compared with the textual description of online tutorials on 8051 programming, such as those found at \url{http://www.8052.com}. 200 201 \subsection{Validation} 202 \label{subsect.validation} 203 179 204 \section{The emulator in Matita} 180 205 \label{sect.emulator.in.matita} 181 206 182 \subsection{What we implement}183 \label{subsect.what.we. implement}207 \subsection{What we do not implement} 208 \label{subsect.what.we.do.not.implement} 184 209 185 210 Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files. … … 191 216 A small library of data structures was written, along with basic functions operating over them. 192 217 Implemented data structures include: Booleans, option types, lists, Cartesian products, Natural numbers, fixed-length vectors, and sparse tries. 218 219 Our type of vectors, in particular, makes heavy use of dependent types. 220 Probing vectors is `type safe' for instance: we cannot index into a vector beyond the vector's length. 193 221 194 222 We represent bits as Boolean values. … … 215 243 We probe a trie with the \texttt{lookup} function. 216 244 This takes an additional argument representing the value to be returned should a stub, representing uninitialised data, be encountered during traversal. 245 246 Like the O'Caml emulator, we use a record to represent processor state: 217 247 218 248 \begin{quote} … … 230 260 special_function_registers_8052: Vector Byte five; 231 261 232 p1_latch: Byte; 233 p3_latch: Byte; 234 235 clock: Time 262 ... 236 263 }. 237 264 \end{lstlisting} 238 265 \end{quote} 239 266 240 % Polymorphic variants 241 242 % Parsing 243 244 % Bitvectors: dependent types 245 246 % Dependent types subtyping 267 However, we `squash' the \texttt{Status} record in the Matita emulator by grouping all 8051 SFRs (respectively, 8052 SFRs) into a single vector of bytes, as opposed to representing them as explicit fields in the record itself. 268 We then provide functions that index into the respective vector to `get' and `set' the respective SFRs. 269 This is due to record typechecking in Matita being slow for large records. 270 271 \subsection{Addressing modes: use of dependent types} 272 \label{subsect.addressing.modes.use.of.dependent.types} 247 273 248 274 \subsection{Dealing with partiality}
Note: See TracChangeset
for help on using the changeset viewer.