Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / memory2 / MOESI_2.lus @ 22fe1c93

History | View | Annotate | Download (2.99 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X and pre Sofar;
5
tel
6

    
7
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool );
8
let
9
    excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or
10
                    X2 and X3 or X2 and X4 or
11
                    X3 and X4 );
12
tel
13

    
14
node moesi(init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool)returns(
15
modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; erreur_mo : bool
16
);
17
var
18
   garde_mo1, garde_mo2, garde_mo3, garde_mo4 : bool;
19
let
20

    
21
   garde_mo1 = pre invalid_mo >= 1;
22
   garde_mo2 = pre exclusive_mo>=1;
23
   garde_mo3 = pre shared_mo + pre owned_mo>=1;
24
   garde_mo4 = pre invalid_mo>=1;
25

    
26
   erreur_mo = false -> exclusive_mo >= 2;
27

    
28
   modified_mo = 0 ->
29
   if(etat_mo1) then if(garde_mo1) then 0 else pre modified_mo else
30
   if(etat_mo2) then if(garde_mo2) then pre modified_mo+1 else pre modified_mo else
31
   if(etat_mo3) then if(garde_mo3) then 0 else pre modified_mo else
32
   if(etat_mo4) then if(garde_mo4) then 0 else pre modified_mo else 
33
   pre modified_mo;
34

    
35
   exclusive_mo = 0 -> 
36
   if(etat_mo1) then if(garde_mo1) then 0 else pre exclusive_mo else
37
   if(etat_mo2) then if(garde_mo2) then pre exclusive_mo-1 else pre exclusive_mo else
38
   if(etat_mo3) then if(garde_mo3) then 1 else pre exclusive_mo else 
39
   if(etat_mo4) then if(garde_mo4) then 1 else pre exclusive_mo else 
40
   pre exclusive_mo;
41

    
42
   shared_mo = 0 ->
43
   if(etat_mo1) then if(garde_mo1) then pre shared_mo + pre exclusive_mo + 1 else pre shared_mo else
44
   if(etat_mo3) then if(garde_mo3) then 0 else pre shared_mo else
45
   if(etat_mo4) then if(garde_mo4) then 0 else pre shared_mo else 
46
   pre shared_mo;
47

    
48
   invalid_mo = init_invalid_mo -> 
49
   if(etat_mo1) then if(garde_mo1) then pre invalid_mo-1 else pre invalid_mo else
50
   if(etat_mo3) then if(garde_mo3) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else
51
   if(etat_mo4) then if(garde_mo4) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else 
52
   pre invalid_mo;
53

    
54
   owned_mo = 0 -> 
55
   if(etat_mo1) then if(garde_mo1) then pre owned_mo + pre modified_mo else pre owned_mo else
56
   if(etat_mo3) then if(garde_mo3) then 0 else pre owned_mo else
57
   if(etat_mo4) then if(garde_mo4) then 0 else pre owned_mo else 
58
   pre owned_mo;
59

    
60
tel
61

    
62
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
63
returns ( OK : bool );
64
    var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
65
        erreur_mo : bool;
66
        env : bool;
67
let
68
    ( modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo, erreur_mo ) =
69
        moesi(init_invalid_mo, etat_mo1, etat_mo2, etat_mo3, etat_mo4 );
70
    env = Sofar( excludes4( etat_mo1, etat_mo2, etat_mo3, etat_mo4 ) );
71
    OK = env => (true ->
72
          (modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo) =
73
          pre(modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo));
74
    --%PROPERTY OK=true;
75
    --%MAIN;
76
tel