Information Technology Reference
In-Depth Information
In Fig. 5, we present the graph corresponding to the formula
:'
,where
G
=
-
edges are represented by dashed lines and
G
6
=
-edges are represented by solid
lines.
The range allocation algorithm has several stages of traversing the graph,
analyzing reachability, removing vertices etc. Without going into the details of
the algorithm, we will present the ranges adequate for this graph, as computed by
the algorithm:
:ZN
c
7! f
N
0
c
7! f
FB
0
c
7! f
1
R
1
;
2
g;
1
g;
1
;
3
g;
FB
c
7! f
1
;
3
g;v
−
7!
2
f
g:
Indeed, every consistent subset of the edges in the graph can be satis-
ed with these ranges. For example, for the subset made of the dashed edges
f
1
;
4
g;
and
v
−
7! f
1
;
4
FB
0
c
)
(FB
0
c
;
N
0
c
)
N
0
c
)
2
1
−
2
(FB
c
;
;
;
(
v
−
;v
) and the solid edge
f
(
v
−
;
g
we can assign
FB
c
=FB
c
=N
c
=1,and
1
−
2
−
= 4. Clearly this assignment satises
the constraints that are represented by these edges.
In this case we reduced the state space from 6
6
to 32. In many cases the
graphs are not as connected as this one, and therefore the reduction in the
state space is much more signicant. Often, 60 - 70% of the variables become
constants, in the same way that N
0
c
became a constant in the example given
above. We once more refer the reader to [17] for further details.
v
=
v
5.5
The Verier Module (TLV)
The validity of the verication conditions is checked by TLV [18], an SMV-based
tool which provides the capability of BDD-programming and has been developed
mainly for nite-state deductive proofs (and is thus convenient in our case for
expressing the renement rule). In the case that the equivalence proof fails, a
counter example is displayed. Since it is possible to isolate the conjunct(s) that
failed the proof, this information can be used by the compiler developer to check
what went wrong. A proof log is generated as part of this process, indicating
what was proved, at what level of abstraction and when.
6 A Case Study
We used CVT to validate an industrial size program, a code generated for the
case study of a turbine developed by SNECMA, which is one of the industrial
case studies in the SACRES project. The program was partitioned manually (by
SNECMA) into 5 units which were separately compiled. Altogether the
Signal
specication is a few thousand lines long and contains more than 1000 variables.
After the abstraction we had about 2000 variables (as explained in Section 5, the
abstraction module replaces function symbols with new variables). Following is
a summary of the results achieved by CVT:
Search WWH ::
Custom Search