Information Technology Reference
In-Depth Information
syntaxes
Ccode
and
AssemblerCode
for the generated SystemC models and As-
semblerCode, respectively, and defining evaluation functions
T
:
type
Ccode =
...
type
AssemblerCode =
...
T
→
IOTS
...
value
:Ccode
T
→
IOTS
...
value
: AssemblerCode
7.6
Abstraction Mappings
When a SystemC model
,there
is a 1-1 correspondence between SystemC variable symbols and assembler vari-
able symbols (e.g. for each SystemC array element
x
[
n
] there is a corresponding
assembler array element
x
(
,n,
4)), except that
M
is compiled into an assembler program
A
A
contains additional local vari-
ables: flags, registers and stack addresses.
We define a SystemC model
+
that extends
with local variable symbols
corresponding to the additional flags, registers and stack addresses in
M
M
A
.E.g.we
add
eax
corresponding to the flag
%eax
.
Then one can obviously define a bijective map
α
M
from the variables in
A
+
. This map will also serve as a map between the variable
to the variables in
M
+
).
For the detailed definitions, see [30].
sets in
T
(
A
)and
T
(
M
7.7
Implementation of a Code Verifier
Currently the code verifier is being implemented in C++. The implementation
consists of the following major components:
-
an implementation of the two
functions yielding IOTS generators for Sys-
temC and assembler code, respectively,
-
a library of transformation rules, and
-
an IOTS transformer that given an IOTS and a transformation rule is able
to apply the transformation rule.
T
A mechanised proof of the equivalence between an assembler program
A
and
the SystemC controller model
from which it is generated is automatically
performed according to the following procedure: The SystemC controller model
M
M
is now mapped to its behavioural IOTS model
T
(
M
), and
A
is mapped
to its model
) as well, using the semantic rules for SystemC and assem-
bler statements, respectively. Next, the symbols of
T
(
A
) are changed to C-style
notation according to mapping
α
M
defined above - this results in
T
(
A
1
.Also,
T
+
), so that
1
the variable symbol space of
T
(
M
) is extended to
T
(
M
T
and
+
) can be directly compared with respect to their variable symbols. Then
the mechanised proof generator analyses
T
(
M
1
with respect to applicable patterns
in the transformation rules. Each pattern application results in a I/O-equivalent
transformation
T
1
2
+
),
T
→T
→
...
until the last transformation results in
T
(
M
whereupon the proof generator terminates.
Search WWH ::
Custom Search