Changeset 3515 for Papers


Ignore:
Timestamp:
Nov 14, 2014, 5:50:34 PM (4 years ago)
Author:
mulligan
Message:

work with jb,dpm from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-assembler-2014/boender-jar-2014.tex

    r3514 r3515  
    5353\label{subsect.matita}
    5454
    55 % CSC
     55Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.
     56It features full spectrum dependent types as well as a sophisticated system of coercions, both of which we exploit in this formalisation.
     57
     58Matita's syntax should be familiar for those readers acquainted with the OCaml functional programming language.
     59Nevertheless, we provide a brief summary of the main syntactic features of Matita:
     60\begin{itemize}
     61\item
     62Non-recursive definitions are introduced with the \texttt{definition} keyword, and recursive definitions with the \texttt{let rec} keywords.
     63\item
     64There is extensive provision for customising syntax (through Unicode). Matita has an advanced system of overloading and resolution so that definitions and proofs look as natural as possible.
     65\end{itemize}
    5666
    5767%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     
    117127
    118128% JB and CSC
     129One of the consequences of using the MCS-51 instruction set is that we have to take its specific branch instructions into account. The MCS-51 has three different types of branch instruction---which one should be used depends on the distance between the instruction and its target. This applies to unconditional branches, conditional branches and procedure calls.
     130
     131The three different types of branch instructions are:
     132\begin{itemize}
     133  \item The {\em short} branch: a 2-byte instruction that can branch over a 1-byte displacement, i.e. XXX bytes forwards or YYY bytes backwards.
     134  \item The {\em absolute} branch: a 2-byte instruction that can change the last 11 bits of the program counter. Thus, it can branch to any destination within the same 2048-byte segment.
     135  \item The {\em long} branch: a 3-byte instruction that can branch to any destination in memory.
     136\end{itemize}
     137
     138Not all combinations of instructions are provided. For example, there is no short call, nor is there a long conditional branch.
     139
     140Apart from their difference in size, the instructions also take different amounts of time to execute: 2 cycles for the short and absolute branch, 3 cycles for the long branch.
     141
     142The {\em branch optimisation problem}, a well-known problem in assembler design, is to find the smallest branch instructions for a given assembler program. This is complicated by the fact that branch instructions can influence each other: the distance between an instruction and its target depends on the size of any branch instructions in between them.
    119143
    120144%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.