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