Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (4 KB)

1

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

    
7
node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool );
8
let
9
    excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
10
                  X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
11
              not X1 and     X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
12
              not X1 and not X2 and     X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
13
              not X1 and not X2 and not X3 and     X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
14
              not X1 and not X2 and not X3 and not X4 and     X5 and not X6 and not X7 and not X8 and not X9 or
15
              not X1 and not X2 and not X3 and not X4 and not X5 and     X6 and not X7 and not X8 and not X9 or
16
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and     X7 and not X8 and not X9 or
17
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and     X8 and not X9 or
18
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and     X9;
19
tel
20

    
21
node illinois(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
22
returns(invalid, dirty, exclusive, shared : int);
23
var
24
   g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool;
25
let
26

    
27
   g1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0;
28
   g2 = pre invalid>=1 and pre dirty>=1;
29
   g3 = pre invalid>=1 and pre shared+pre exclusive>=1;
30
   g4 = pre exclusive>=1;
31
   g5 = pre shared>=1;
32
   g6 = pre invalid>=1;
33
   g7 = pre dirty>=1;
34
   g8 = pre shared>=1;
35
   g9 = pre exclusive>=1;
36

    
37
   invalid = (if(init_invalid>0) then init_invalid else 1-init_invalid) ->
38
   if(e1) then if(g1) then pre invalid-1 else pre invalid else 
39
   if(e2) then if(g2) then pre invalid-1 else pre invalid else 
40
   if(e3) then if(g3) then pre invalid-1 else pre invalid else 
41
   if(e5) then if(g5) then pre invalid+pre shared-1 else pre invalid else 
42
   if(e6) then if(g6) then pre invalid+pre dirty+pre shared+pre exclusive-1 else pre invalid else 
43
   if(e7) then if(g7) then pre invalid+1 else pre invalid else 
44
   if(e8) then if(g8) then pre invalid+1 else pre invalid else 
45
   if(e9) then if(g9) then pre invalid+1 else pre invalid else 
46
   pre invalid;
47

    
48
   dirty = 0 -> 
49
   if(e2) then if(g2) then pre dirty-1 else pre dirty else 
50
   if(e4) then if(g4) then pre dirty+1 else pre dirty else 
51
   if(e5) then if(g5) then pre dirty+1 else pre dirty else 
52
   if(e6) then if(g6) then 1 else pre dirty else 
53
   if(e7) then if(g7) then pre dirty-1 else pre dirty else 
54
   pre dirty;
55

    
56
   exclusive = 0 -> 
57
   if(e1) then if(g1) then pre exclusive+1 else pre exclusive else 
58
   if(e3) then if(g3) then pre 0 else pre exclusive else 
59
   if(e4) then if(g4) then pre exclusive-1 else pre exclusive else 
60
   if(e6) then if(g6) then 0 else pre exclusive else 
61
   if(e9) then if(g9) then pre exclusive-1 else pre exclusive else 
62
   pre exclusive;
63

    
64
   shared = 0 -> 
65
   if(e2) then if(g2) then pre shared+2 else pre shared else 
66
   if(e3) then if(g3) then pre shared+pre exclusive+1 else pre shared else 
67
   if(e5) then if(g5) then 0 else pre shared else 
68
   if(e6) then if(g6) then 0 else pre shared else 
69
   if(e8) then if(g8) then pre shared-1 else pre shared else 
70
   pre shared;
71

    
72
tel
73

    
74
-- NOTE: Not provable!
75
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)
76
returns( OK : bool);
77
    var invalid, dirty, exclusive, shared : int;
78
        R3, A1, A2, A3 : bool;
79
        env : bool;
80
let
81
    ( invalid, dirty, exclusive, shared ) =
82
        illinois( e1, e2, e3, e4, e5, e6, e7, e8, e9, init_invalid );
83

    
84
    env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) );
85

    
86
    A1 = true; --env => invalid >= 0; -- incorrect
87
    A2 = env => dirty >= 0;
88
    A3 = env => exclusive >= 0;
89
    R3 = env => dirty < 2;
90
    OK = A1 and A1 and A3 and R3;
91
    --%PROPERTY OK=true;
92
    --%MAIN;
93
tel