lustrec / test / src / kind_fmcad08 / misc / _6counter2.lus @ 0cbf0839
History | View | Annotate | Download (394 Bytes)
1 |
-- a simple 0 to 5 boolean counter (A is LSB, C is MSB) |
---|---|
2 |
-- invalid property is that it should never reach 5 or 7 |
3 |
|
4 |
node top (x:bool) returns (OK:bool); |
5 |
var a,b,c:bool; |
6 |
let |
7 |
a = false -> not pre(a); |
8 |
b = false -> (not pre(c) and not pre(b) and pre(a)) or |
9 |
(pre(b) and not pre(a)); |
10 |
c = false -> (pre(c) and not pre(a)) or (pre(b) and pre(a)); |
11 |
OK= (c and a); |
12 |
--%PROPERTY OK; |
13 |
tel |