1 | ###################################################################### |
---|
2 | # Properties of the decoder. |
---|
3 | ###################################################################### |
---|
4 | |
---|
5 | #PASS: The all-zero state is never re-entered. |
---|
6 | X G !decoder.state[9:0]=0; |
---|
7 | |
---|
8 | #PASS: The output is never 255. |
---|
9 | G !plain[7:0]=255; |
---|
10 | |
---|
11 | #PASS: No two consecutive states have plain != 0. |
---|
12 | G(plain[7:0]=0 + X plain[7:0]=0); |
---|
13 | |
---|
14 | #PASS: String 010 is decoded as E. |
---|
15 | G((decoder.state[9:0]=0 + decoder.leaf=1) -> |
---|
16 | X(ci=0 -> X(ci=1 -> X(ci=0 -> plain[7:0]=69)))); |
---|
17 | |
---|
18 | #FAIL: in this property, "plain" is strobed one clock cycle too late. |
---|
19 | G((decoder.state[9:0]=0 + decoder.leaf=1) -> |
---|
20 | X(ci=0 -> X(ci=1 -> X(ci=0 -> X plain[7:0]=69)))); |
---|
21 | |
---|
22 | #PASS: String 00000 is decoded as U. |
---|
23 | G((decoder.state[9:0]=0 + decoder.leaf=1) -> |
---|
24 | X(ci=0 -> X(ci=0 -> X(ci=0 -> X(ci=0 -> X(ci=0 -> plain[7:0]=85)))))); |
---|
25 | |
---|
26 | |
---|
27 | ###################################################################### |
---|
28 | # Properties of the encoder. |
---|
29 | ###################################################################### |
---|
30 | |
---|
31 | #PASS: The encoder shift register is never 0. |
---|
32 | G !encoder.shiftreg[9:0]=0; |
---|
33 | |
---|
34 | |
---|
35 | ###################################################################### |
---|
36 | # Global properties. |
---|
37 | ###################################################################### |
---|
38 | |
---|
39 | #PASS: When a new transmission begins, the decoder is ready. |
---|
40 | G(encoder.shiftreg[9:1]=1 -> X decoder.leaf=1); |
---|
41 | |
---|
42 | #PASS: Characters are successfully transmitted. (Two equivalent forms.) |
---|
43 | G(decoder.leaf=1 -> plain[7:0]==ch[7:0]); |
---|
44 | G(plain[7:0]=0 + plain[7:0]==ch[7:0]); |
---|