Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.69 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X and pre Sofar;
5
tel
6
node Abs( X : int ) returns ( Abs : int );
7
let
8
    Abs = if X < 0 then -X else X;
9
tel
10
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool );
11
let
12
    excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or
13
                    X2 and X3 or X2 and X4 or
14
                    X3 and X4 );
15
tel
16
node mesi(etat_me1, etat_me2, etat_me3, etat_me4 : bool
17
) returns (
18
   modified_me, exclusive_me, shared_me, invalid_me : int
19
);
20
var
21
   garde_me1, garde_me2, garde_me3, garde_me4 : bool;
22
let
23
   garde_me1 = pre invalid_me >= 1;
24
   garde_me2 = pre exclusive_me>=1;
25
   garde_me3 = pre shared_me>=1;
26
   garde_me4 = pre invalid_me>=1;
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
   exclusive_me = 0 -> 
34
   if(etat_me1) then if(garde_me1) then 0 else pre exclusive_me else
35
   if(etat_me2) then if(garde_me2) then pre exclusive_me -1 else pre exclusive_me else 
36
   if(etat_me3) then if(garde_me3) then 1 else pre exclusive_me else
37
   if(etat_me4) then if(garde_me4) then 1 else pre exclusive_me else 
38
   pre exclusive_me;
39
   shared_me = 0 -> 
40
   if(etat_me1) then if(garde_me1) then pre shared_me -1+ pre exclusive_me + pre modified_me -1- 1 else pre shared_me else 
41
   if(etat_me2)	then if(garde_me2) then pre shared_me else pre shared_me else 
42
   if(etat_me3)	then if(garde_me3) then 0 else pre shared_me else
43
   if(etat_me4) then if(garde_me4) then 0 else pre shared_me else 
44
   pre shared_me;
45
   invalid_me = 3 ->
46
   if(etat_me1) then if(garde_me1) then pre invalid_me -1 else pre invalid_me else
47
   if(etat_me2)	then if(garde_me2) then pre invalid_me else pre invalid_me else
48
   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 
49
   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 
50
   pre invalid_me;
51
tel
52
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
53
    var modified_me, exclusive_me, shared_me, invalid_me : int;
54
        env : bool;
55
let
56
    ( modified_me, exclusive_me, shared_me, invalid_me ) =
57
        mesi( etat_me1, etat_me2, etat_me3, etat_me4 );
58
    env = Sofar( excludes4( etat_me1, etat_me2, etat_me3, etat_me4 ) );
59
    OK = env => (Abs(modified_me)+Abs(exclusive_me)+
60
                 Abs(shared_me)+Abs(invalid_me)) <= 3;
61
  --%MAIN;
62
  --%PROPERTY  OK=true;
63
tel