lustrec / test / src / kind_fmcad08 / memory2 / MESI_i1_e2_1758_e8_12.lus @ 22fe1c93
History | View | Annotate | Download (2.65 KB)
1 |
|
---|---|
2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
3 |
let |
4 |
Sofar = X -> X and pre Sofar; |
5 |
tel |
6 |
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool ); |
7 |
let |
8 |
excludes = not ( X1 and X2 and X1 and X3 or X1 and X4 or |
9 |
X2 and X3 or X2 and X4 or |
10 |
X3 and X4 ); |
11 |
tel |
12 |
node mesi(etat_me1, etat_me2, etat_me3, etat_me4 : bool |
13 |
) returns ( |
14 |
modified_me, exclusive_me, shared_me, invalid_me : int |
15 |
); |
16 |
var |
17 |
garde_me1, garde_me2, garde_me3, garde_me4 : bool; |
18 |
let |
19 |
garde_me1 = pre invalid_me >= 1; |
20 |
garde_me2 = pre exclusive_me>=1; |
21 |
garde_me3 = pre shared_me>=1; |
22 |
garde_me4 = pre invalid_me>=1; |
23 |
modified_me = 0 -> |
24 |
if(etat_me1) then if(garde_me1) then 0 else pre modified_me else |
25 |
if(etat_me2) then if(garde_me2) then pre modified_me -1 else pre modified_me else |
26 |
if(etat_me3) then if(garde_me3) then 0 else pre modified_me else |
27 |
if(etat_me4) then if(garde_me4) then 0 else pre modified_me else |
28 |
pre modified_me; |
29 |
exclusive_me = 0 -> |
30 |
if(etat_me1) then if(garde_me1) then 0 else pre exclusive_me else |
31 |
if(etat_me2) then if(garde_me2) then pre exclusive_me -1 else pre exclusive_me else |
32 |
if(etat_me3) then if(garde_me3) then 1 else pre exclusive_me else |
33 |
if(etat_me4) then if(garde_me4) then 1 else pre exclusive_me else |
34 |
pre exclusive_me; |
35 |
shared_me = 0 -> |
36 |
if(etat_me1) then if(garde_me1) then pre shared_me -1+ pre exclusive_me + pre modified_me - 1 else pre shared_me else |
37 |
if(etat_me2) then if(garde_me2) then pre shared_me else pre shared_me else |
38 |
if(etat_me3) then if(garde_me3) then 0 else pre shared_me else |
39 |
if(etat_me4) then if(garde_me4) then 0 else pre shared_me else |
40 |
pre shared_me; |
41 |
invalid_me = 3 -> |
42 |
if(etat_me1) then if(garde_me1) then pre invalid_me -1 else pre invalid_me else |
43 |
if(etat_me2) then if(garde_me2) then pre invalid_me else pre invalid_me else |
44 |
if(etat_me3) then if(garde_me3) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else |
45 |
if(etat_me4) then if(garde_me4) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else |
46 |
pre invalid_me; |
47 |
tel |
48 |
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool ); |
49 |
var modified_me, exclusive_me, shared_me, invalid_me : int; |
50 |
env : bool; |
51 |
let |
52 |
( modified_me, exclusive_me, shared_me, invalid_me ) = |
53 |
mesi( etat_me1, etat_me2, etat_me3, etat_me4 ); |
54 |
env = Sofar( excludes4( etat_me1, etat_me2, etat_me3, etat_me4 ) ); |
55 |
OK = env => (true -> (modified_me+exclusive_me+shared_me+invalid_me) = |
56 |
pre(modified_me+exclusive_me+shared_me+invalid_me)); |
57 |
--%MAIN; |
58 |
--%PROPERTY OK=true; |
59 |
tel |