1 sort bitvec 1
2 input 1 reset
3 input 1 iStartSignal ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 92:24]
4 sort bitvec 16
5 state 4 counter ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 96:13]
; _resetCount.init
6 zero 1
7 state 1 _resetCount
8 init 1 7 6
9 zero 1
10 uext 4 9 15
11 eq 1 5 10 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 98:32]
12 and 1 3 11 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 98:21]
13 sort bitvec 17
14 const 4 0000000000000100
15 uext 13 14 1
16 one 1
17 uext 13 16 16
18 sub 13 15 17 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 99:26]
19 slice 4 18 15 0 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 99:26]
20 zero 1
21 uext 4 20 15
22 neq 1 5 21 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 100:22]
23 uext 13 5 1
24 one 1
25 uext 13 24 16
26 sub 13 23 25 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 101:24]
27 slice 4 26 15 0 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 101:24]
28 ite 4 22 27 5 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 100:31 101:13 96:13]
29 const 4 0000000000000100
30 ugte 1 5 29
31 not 1 30 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 104:18]
32 not 1 2 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 104:9]
33 not 1 31 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 104:9]
34 one 1
35 ugte 1 7 34
36 not 1 35
37 zero 1
38 uext 4 37 15
39 neq 1 5 38 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 93:17], @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 103:20]
40 implies 1 32 31
41 not 1 40
42 bad 41 ; assert @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 104:9]
43 implies 1 36 2
44 constraint 43 ; _resetActive
; counter.next
45 ite 4 12 19 28
46 next 4 5 45
; _resetCount.next
47 sort bitvec 2
48 uext 47 7 1
49 one 1
50 uext 47 49 1
51 add 47 48 50
52 slice 1 51 0 0
53 ite 1 36 52 7
54 next 1 7 53