[105] | 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]); |
---|