The Software Package BALM - The Unknown Component Problem: Theory and Applications - page 134

.p 64
0 st0 st0 0
1 st0 st1 1
0 st1 st1 0
1 st1 st2 1
...
0 st30 st30 0
1 st30 st31 1
0 st31 st31 0
1 st31 st0 1
.end
We may describe it in the BLIF-MV format (say in the file counter32.mv ) 2 :
.model counter32.mv
.inputs i
.outputs SP o
.mv SF, SP 32 st0 st1 ... st31
.table i SP ->SF
0 st0 st0
1 st0 st1
0 st1 st1
1 st1 st2
...
0 st31 st31
1 st31 st0
.latch SF SP
.reset SP
0
.table i SP ->o
0 st0 0
1 st0 1
0 st1 0
1 st1 1
...
0 st31 0
1 st31 1
.end
Otherwise, we could describe it in the AUT format as follows (say in the file
counter32.aut ):
.model counter32.aut
.inputs i o
.outputs Acc
.mv CS, NS 32 st0 st1 ... st31
.latch NS CS
.reset CS
0
2 Lines introducing mv variables like .mv SF, SP 32 st0 st1 ... st31 stand for the full list of symbolic
names of the values of the mv variables, e.g., .mv SF, SP 32 st0 st1 st2 st3 st4 st5 st6 st7 st8 st9
st10 st11 st12 st13 st14 st15 st16 st17 st18 st19 st20 st21 st22 st23 st24 st25 st26 st27 st28 st29
st39 st31.