Information Technology Reference
In-Depth Information
From these denitions and the axioms of the base model we can prove the fol-
lowing theorem:
Theorem 1 (I1-instruction theorem).
I 1 (
a;
instr (
n
)
b
)
Oreg := Oreg bitor n
;
E 1 ( instr );
I 1 (
a
instr (
n
)
;b
) .
Here we write instr (
) for the code sequence consisting of the single instruction
instr with four-bit operand
n
16. This theorem formally reflects that
a machine program that is loaded and started at some instruction instr with
four-bit operand
n
,0
n<
n
behaves as follows:
n
is bitwisely or-ed with the value in the
operand register (this loads
to the least four bits of the operand register since
every previous instruction leaves these bits cleared), and then the (abstracted)
eect of instr is executed. Afterwards it behaves as if the same program is
executed starting at the next instruction.
Moreover, we prove for each instruction instr approximations for
n
E 1 ( instr )
that do not refer to
E 0 . An example for the ldl instruction can be found in
Table 1.
Large Operands for Instructions. The purpose of the Transputer's operand
register Oreg is to provide word-size operands for the instructions. The idea is
that the operand register is lled with the operand in portions of four bits by
a sequence of pfix and nfix instructions preceding the instruction for the ac-
tual function, the operand part of which provides the least signicant four bits
only. This special purpose and use of the operand register, however, is not di-
rectly reflected in the behavioral description of the Transputer we have available
up-to-now, where Oreg is treated like any other register. The second abstrac-
tion, therefore, provides an understanding of leading pfix and nfix sequences
together with a trailing non- pfix and non- nfix instruction as a multi-byte in-
struction.
We dene a new view
I 2 (
a;b
) based on
I 1 (
a;b
) and an abstraction
E 2 ( instr
;w
)
of an instruction instr 's eect together with a word operand
w
. 4
We then can
prove a new version of the instruction theorem:
Theorem 2 (I2-instruction theorem).
I 2 (
a;
instr (
w
)
b
)
E 2 ( instr
;w
);
I 2 (
a
instr (
w
)
;b
) .
Now instr (
) stands for the instruction sequence resulting from the standard
scheme for generating pfix and nfix instructions described in [23, Chapter 4].
Furthermore we prove approximations for
w
E 2 as shown for the ldl -instruction
in Table 1. Note that the I2-instruction theorem is easier to apply than the old
I1-instruction theorem as it requires no explicit calculations with the operand
register.
4 The range of word operands diers for the dierent processors from the Transputer
family. A typically value is 2 31 w< 2 31 for 32-bit Transputers but there are also
16-bit Transputers for which the range is 2 15 w< 2 15 .
 
Search WWH ::




Custom Search