Information Technology Reference
In-Depth Information
7.8 Example
We illustrate the mechanised proof procedure explained above using a fragment
of the SystemC controller code from our case study. Here global shadow variables
reqsigNext[i]
(the new state required for signal
i
)and
reqptNext[j]
(the
new state required for point
j
are copied to output signals
reqsig[i]
(set-
state request to signal
i
)and
reqpt[j]
(set-state request to point
j
) during the
output phase of a main loop cycle. Consider the following fragment from the
output phase of a SystemC controller
M
:
for ( int i=0; i<NUM_SIGNALS; i++)
reqsig[i] = reqsigNext[i];
for ( int j=0; j<NUM_POINTS; j++)
reqpt[j] = reqptNext[j];
The concrete configuration data for this controller instance defines
NUM POINTS=3
and
NUM SIGNALS=3
. From that the compiler
3
generates the following assembler
fragment of
A
:
movl $0, i
jmp .L103
.L104:
movl i, %edx
movl i, %eax
movl reqsigNext(,%eax,4), %eax
movl %eax, reqsig(,%edx,4)
movl i, %eax
incl %eax
movl %eax, i
.L103:
movl i, %eax
cmpl $2, %eax
jle .L104
movl $0, j
jmp .L106
.L107:
movl j, %edx
movl j, %eax
movl reqptNext(,%eax,4), %eax
movl %eax, reqpt(,%edx,4)
movl j, %eax
incl %eax
movl %eax, j
.L106:
movl j, %eax
cmpl $2, %eax
jle .L107
3
We have used
gcc 4.0.2
for this example.
Search WWH ::
Custom Search