Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.54 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 mesi(etat_me1, etat_me2, etat_me3, etat_me4 : bool
15
) returns (
16
   modified_me, exclusive_me, shared_me, invalid_me : int
17
);
18
var
19
   garde_me1, garde_me2, garde_me3, garde_me4 : bool;
20
let
21

    
22
   garde_me1 = pre invalid_me >= 1;
23
   garde_me2 = pre exclusive_me>=1;
24
   garde_me3 = pre shared_me>=1;
25
   garde_me4 = pre invalid_me>=1;
26

    
27
   modified_me = 0 ->
28
   if(etat_me1) then if(garde_me1) then 0 else pre modified_me else 
29
   if(etat_me2) then if(garde_me2) then pre modified_me -1 else pre modified_me else
30
   if(etat_me3)	then if(garde_me3) then 0 else pre modified_me else 
31
   if(etat_me4) then if(garde_me4) then 0 else pre modified_me else 
32
   pre modified_me;
33

    
34
   exclusive_me = 0 -> 
35
   if(etat_me1) then if(garde_me1) then 0 else pre exclusive_me else
36
   if(etat_me2) then if(garde_me2) then pre exclusive_me -1 else pre exclusive_me else 
37
   if(etat_me3) then if(garde_me3) then 1 else pre exclusive_me else
38
   if(etat_me4) then if(garde_me4) then 1 else pre exclusive_me else 
39
   pre exclusive_me;
40

    
41
   shared_me = 0 -> 
42
   if(etat_me1) then if(garde_me1) then pre shared_me + pre exclusive_me + pre modified_me - 1 else pre shared_me else 
43
   if(etat_me2)	then if(garde_me2) then pre shared_me else pre shared_me else 
44
   if(etat_me3)	then if(garde_me3) then 0 else pre shared_me else
45
   if(etat_me4) then if(garde_me4) then 0 else pre shared_me else 
46
   pre shared_me;
47

    
48
   invalid_me = 3 ->
49
   if(etat_me1) then if(garde_me1) then pre invalid_me -1 else pre invalid_me else
50
   if(etat_me2)	then if(garde_me2) then pre invalid_me else pre invalid_me else
51
   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 
52
   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 
53
   pre invalid_me;
54

    
55
tel
56

    
57
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
58
    var modified_me, exclusive_me, shared_me, invalid_me : int;
59
        env : bool;
60
let
61
    ( modified_me, exclusive_me, shared_me, invalid_me ) =
62
        mesi( etat_me1, etat_me2, etat_me3, etat_me4 );
63
    env = Sofar( excludes4( etat_me1, etat_me2, etat_me3, etat_me4 ) );
64
    OK = env => shared_me >= 0;
65
    --%PROPERTY OK=true;
66
    --%MAIN;
67
tel