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