lustrec / test / src / kind_fmcad08 / misc / switch2.lus @ 0cbf0839
History | View | Annotate | Download (712 Bytes)
1 |
node SWITCH1 (set,reset,initial:bool) returns (level:bool); |
---|---|
2 |
let |
3 |
level = initial -> if set then true |
4 |
else if reset then false |
5 |
else pre(level); |
6 |
tel |
7 |
|
8 |
node SWITCH (set,reset,initial:bool) returns (level:bool); |
9 |
let |
10 |
level = initial -> if set and not pre(level) then true |
11 |
else if reset then false |
12 |
else pre(level); |
13 |
tel |
14 |
|
15 |
--requires assert to be true |
16 |
node top(set, treset, initial:bool) returns (OK:bool); |
17 |
var level,level1:bool; |
18 |
let |
19 |
level = SWITCH(set,treset,initial); |
20 |
level1 = SWITCH1(set,treset,initial); |
21 |
OK = if not(set and treset) then(level = level1) else true; |
22 |
-- assert not(set and treset); |
23 |
--%PROPERTY OK=true; |
24 |
tel |