Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.73 KB)

1

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

    
7
node Abs( X : int ) returns ( Abs : int );
8
let
9
    Abs = if X < 0 then -X else X;
10
tel
11

    
12
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool );
13
let
14
    excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or
15
                    X2 and X3 or X2 and X4 or
16
                    X3 and X4 );
17
tel
18

    
19
node mesi(etat_me1, etat_me2, etat_me3, etat_me4 : bool
20
) returns (
21
   modified_me, exclusive_me, shared_me, invalid_me : int
22
);
23
var
24
   garde_me1, garde_me2, garde_me3, garde_me4 : bool;
25
let
26

    
27
   garde_me1 = pre invalid_me >= 1;
28
   garde_me2 = pre exclusive_me>=1;
29
   garde_me3 = pre shared_me>=1;
30
   garde_me4 = pre invalid_me>=1;
31

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

    
39
   exclusive_me = 0 -> 
40
   if(etat_me1) then if(garde_me1) then 0 else pre exclusive_me else
41
   if(etat_me2) then if(garde_me2) then pre exclusive_me -1 else pre exclusive_me else 
42
   if(etat_me3) then if(garde_me3) then 1 else pre exclusive_me else
43
   if(etat_me4) then if(garde_me4) then 1 else pre exclusive_me else 
44
   pre exclusive_me;
45

    
46
   shared_me = 0 -> 
47
   if(etat_me1) then if(garde_me1) then pre shared_me + pre exclusive_me + pre modified_me - 1 else pre shared_me else 
48
   if(etat_me2)	then if(garde_me2) then pre shared_me else pre shared_me else 
49
   if(etat_me3)	then if(garde_me3) then 0 else pre shared_me else
50
   if(etat_me4) then if(garde_me4) then 0 else pre shared_me else 
51
   pre shared_me;
52

    
53
   invalid_me = 3 ->
54
   if(etat_me1) then if(garde_me1) then pre invalid_me -1 else pre invalid_me else
55
   if(etat_me2)	then if(garde_me2) then pre invalid_me else pre invalid_me else
56
   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 
57
   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 
58
   pre invalid_me;
59

    
60
tel
61

    
62
-- Only provable in nbac
63
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
64
    var modified_me, exclusive_me, shared_me, invalid_me : int;
65
        env : bool;
66
let
67
    ( modified_me, exclusive_me, shared_me, invalid_me ) =
68
        mesi( etat_me1, etat_me2, etat_me3, etat_me4 );
69
    env = Sofar( excludes4( etat_me1, etat_me2, etat_me3, etat_me4 ) );
70
    OK = env => (Abs(modified_me)+Abs(exclusive_me)+
71
                 Abs(shared_me)+Abs(invalid_me)) <= 3;
72
    --%PROPERTY OK=true;
73
    --%MAIN;
74
tel