Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / memory1 / FIREFLY_9.lus @ 22fe1c93

History | View | Annotate | Download (3.76 KB)

1 22fe1c93 ploc
--
2
-- Source: David Merchat (node firefly)
3
--
4
5
node First( X : int ) returns ( First : int );
6
let
7
    First = X -> pre First;
8
tel
9
10
node Sofar( X : bool ) returns ( Sofar : bool );
11
let
12
    Sofar = X -> X and pre Sofar;
13
tel
14
15
node excludes8( X1, X2, X3, X4, X5, X6, X7, X8 : bool ) returns ( excludes : bool );
16
let
17
    excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
18
                  X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
19
              not X1 and     X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
20
              not X1 and not X2 and     X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
21
              not X1 and not X2 and not X3 and     X4 and not X5 and not X6 and not X7 and not X8 or
22
              not X1 and not X2 and not X3 and not X4 and     X5 and not X6 and not X7 and not X8 or
23
              not X1 and not X2 and not X3 and not X4 and not X5 and     X6 and not X7 and not X8 or
24
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and     X7 and not X8 or
25
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and     X8;
26
tel
27
28
node firefly(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) 
29
	returns(invalid, dirty, exclusive, shared : int);
30
var
31
32
	garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8 : bool;
33
	mem_invalid : int;
34
35
let
36
37
	mem_invalid = i_invalid -> pre mem_invalid;
38
39
	garde1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 ;
40
	garde2 = pre invalid>=1 and pre dirty>=1;
41
	garde3 = pre invalid>=1 and pre shared+pre exclusive>=1;
42
	garde4 = pre exclusive>=1;
43
	garde5 = pre shared=1;
44
	garde6 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0;
45
	garde7 = pre invalid>=1 and pre dirty>=1;
46
	garde8 = pre invalid>=1 and pre shared+pre exclusive>=1;
47
48
	invalid = mem_invalid ->
49
	if(e1) then if(garde1) then pre invalid-1 else pre invalid else
50
	if(e2) then if(garde2) then pre invalid-1 else pre invalid else
51
	if(e3) then if(garde3) then pre invalid-1 else pre invalid else
52
	if(e6) then if(garde6) then pre invalid-1 else pre invalid else
53
	if(e7) then if(garde7) then pre invalid-1 else pre invalid else
54
	if(e8) then if(garde8) then pre invalid-1 else pre invalid else
55
	pre invalid;
56
	
57
58
	dirty = 0 -> 
59
	if(e2) then if(garde2) then pre dirty-1 else pre dirty else
60
	if(e4) then if(garde4) then pre dirty+1 else pre dirty else
61
	if(e6) then if(garde6) then 1 else pre dirty else
62
	if(e7) then if(garde7) then pre dirty-1 else pre dirty else
63
	pre dirty;
64
65
	exclusive = 0 -> 
66
	if(e1) then if(garde1) then pre exclusive+1 else pre exclusive else
67
	if(e3) then if(garde3) then 0 else pre exclusive else 
68
	if(e4) then if(garde4) then pre exclusive-1 else pre exclusive else
69
	if(e5) then if(garde5) then pre exclusive+1 else pre exclusive else
70
	if(e8) then if(garde8) then 0 else pre exclusive else
71
	pre exclusive;
72
73
	shared = 0 ->
74
	if(e2) then if(garde2) then pre shared+2 else pre shared else
75
	if(e3) then if(garde3) then pre shared + pre exclusive + 1 else pre shared else
76
	if(e5) then if(garde5) then pre 0 else pre shared else
77
	if(e7) then if(garde7) then pre shared+2 else pre shared else
78
	if(e8) then if(garde8) then pre shared + pre exclusive + 1 else pre shared else
79
	pre shared;
80
81
tel
82
83
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) 
84
	returns( OK : bool );
85
    var invalid, dirty, exclusive, shared : int;
86
        env : bool;
87
        procs : int;
88
let
89
    ( invalid, dirty, exclusive, shared ) =
90
        firefly( e1, e2, e3, e4, e5, e6, e7, e8, i_invalid );
91
92
    env = Sofar( excludes8( e1, e2, e3, e4, e5, e6, e7, e8 ) and
93
                 i_invalid >= 0 and i_invalid < 5 );
94
    procs = First( i_invalid );
95
96
    OK = env => invalid <= procs;
97
    --%PROPERTY OK=true;
98
    --%MAIN;
99
tel