Changeset 3515

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

work with jb,dpm from today

File:
1 edited

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

 r3514 \label{subsect.matita} % CSC Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. It features full spectrum dependent types as well as a sophisticated system of coercions, both of which we exploit in this formalisation. Matita's syntax should be familiar for those readers acquainted with the OCaml functional programming language. Nevertheless, we provide a brief summary of the main syntactic features of Matita: \begin{itemize} \item Non-recursive definitions are introduced with the \texttt{definition} keyword, and recursive definitions with the \texttt{let rec} keywords. \item There 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. \end{itemize} %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % JB and CSC One 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. The three different types of branch instructions are: \begin{itemize} \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. \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. \item The {\em long} branch: a 3-byte instruction that can branch to any destination in memory. \end{itemize} Not all combinations of instructions are provided. For example, there is no short call, nor is there a long conditional branch. Apart 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. The {\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.