Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.73 KB)

1 22fe1c93 ploc
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X and pre Sofar;
5
tel
6
7
node excludes3( X1, X2, X3 : bool ) returns ( excludes : bool );
8
let
9
    excludes = not ( X1 and X2 or X1 and X3 or X2 and X3 );
10
tel
11
12
node synapse(e_s1, e_s2, e_s3 : bool; init_invalid_s : int) 
13
returns(invalid_s, valid_s, dirty_s : int; mem_init_s : int );
14
var
15
	garde_s1, garde_s2, garde_s3 : bool;
16
17
let
18
19
	garde_s1 = pre invalid_s>=1;
20
	garde_s2 = pre valid_s>=1;
21
	garde_s3 = pre invalid_s>=1;
22
23
	mem_init_s = init_invalid_s -> pre mem_init_s;
24
25
	invalid_s = mem_init_s -> 
26
	if(e_s1) then if(garde_s1) then pre invalid_s + pre dirty_s -1 else pre invalid_s else
27
	if(e_s2) then if(garde_s2) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else
28
	if(e_s3) then if(garde_s3) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else 
29
	pre invalid_s;
30
31
	valid_s = 0 ->
32
	if(e_s1) then if(garde_s1) then pre valid_s +1 else pre valid_s else
33
	if(e_s2) then if(garde_s2) then 0 else pre valid_s else
34
	if(e_s3) then if(garde_s3) then 0 else pre valid_s else 
35
	pre valid_s;
36
37
	dirty_s = 0 ->
38
	if(e_s1) then if(garde_s1) then 0 else pre dirty_s else 
39
	if(e_s2) then if(garde_s2) then 1 else pre dirty_s else 
40
	if(e_s3) then if(garde_s3) then 1 else pre dirty_s else 
41
	pre dirty_s;
42
43
tel
44
45
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
46
returns( OK : bool );
47
    var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
48
        env : bool;
49
let
50
    ( invalid_s, valid_s, dirty_s, mem_init_s ) = 
51
        synapse(e_s1, e_s2, e_s3, init_invalid_s );
52
53
    env = Sofar( excludes3(e_s1, e_s2, e_s3) and init_invalid_s >= 0 );
54
55
    OK = env => (true -> invalid_s+valid_s+dirty_s = pre(invalid_s+valid_s+dirty_s));
56
    --%PROPERTY OK=true;
57
    --%MAIN;
58
tel