Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.59 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X or pre Sofar;
5
tel
6
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool );
7
let
8
    excludes = not ( X1 or X2 or 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 + 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 ) and
55
                 modified_me >= 0 );
56
    OK = env => modified_me <= 1 or shared_me <= 1;
57
  --%MAIN;
58
  --%PROPERTY  OK=true;
59
tel