Changeset 3515 for Papers

Nov 14, 2014, 5:50:34 PM (4 years ago)

work with jb,dpm from today

1 edited


  • Papers/jar-assembler-2014/boender-jar-2014.tex

    r3514 r3515  
    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.
     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:
     62Non-recursive definitions are introduced with the \texttt{definition} keyword, and recursive definitions with the \texttt{let rec} keywords.
     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.
    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.
     131The three different types of branch instructions are:
     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.
     138Not all combinations of instructions are provided. For example, there is no short call, nor is there a long conditional branch.
     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.
     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.
Note: See TracChangeset for help on using the changeset viewer.