1 sort bitvec 1
2 input 1 reset
3 input 1 iStartSignal ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 112:24]
4 sort bitvec 16
5 state 4 counter ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 113:24]
6 state 1 REG ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 125:21]
; _resetCount.init
7 zero 1
8 state 1 _resetCount
9 init 1 8 7
10 zero 1
11 uext 4 10 15
12 eq 1 5 11 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 114:32]
13 and 1 3 12 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 114:21]
14 zero 1
15 uext 4 14 15
16 neq 1 5 15 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 116:22]
17 sort bitvec 17
18 uext 17 5 1
19 one 1
20 uext 17 19 16
21 sub 17 18 20 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 117:24]
22 slice 4 21 15 0 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 117:24]
23 ite 4 16 22 5 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 116:31 117:13 113:24]
24 sort bitvec 2
25 ones 24
26 uext 4 25 14
27 ite 4 13 26 23 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 114:41 115:13]
28 sort bitvec 3
29 const 28 100
30 uext 4 29 13
31 ugte 1 5 30
32 not 1 31 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 120:18]
33 not 1 2 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 120:9]
34 not 1 32 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 120:9]
35 not 1 3 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 124:14]
36 not 1 35 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 124:13]
37 not 1 6 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 125:13]
38 one 1
39 ugte 1 8 38
40 not 1 39
41 implies 1 33 32
42 not 1 41
43 bad 42 ; assert @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 120:9]
44 implies 1 33 35
45 constraint 44 ; assume @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 124:13]
46 implies 1 33 6
47 not 1 46
48 bad 47 ; assert_1 @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 125:13]
49 implies 1 40 2
50 constraint 49 ; _resetActive
; counter.next
51 zero 4
52 ite 4 2 51 27
53 next 4 5 52
; REG.next
54 zero 1
55 uext 4 54 15
56 eq 1 5 55
57 next 1 6 56
; _resetCount.next
58 uext 24 8 1
59 one 1
60 uext 24 59 1
61 add 24 58 60
62 slice 1 61 0 0
63 ite 1 40 62 8
64 next 1 8 63