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