1 sort bitvec 1
2 input 1 reset
3 sort bitvec 16
4 state 3 counter ; @[d/chiseltest/src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 82:24]
; _resetCount.init
5 zero 1
6 state 1 _resetCount
7 init 1 6 5
8 sort bitvec 17
9 uext 8 4 1
10 one 1
11 uext 8 10 16
12 add 8 9 11 ; @[d/chiseltest/src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 83:22]
13 slice 3 12 15 0 ; @[d/chiseltest/src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 83:22]
14 sort bitvec 4
15 const 14 1010
16 uext 3 15 12
17 ugt 1 4 16
18 not 1 17 ; @[d/chiseltest/src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 84:18]
19 not 1 2 ; @[d/chiseltest/src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 84:9]
20 not 1 18 ; @[d/chiseltest/src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 84:9]
21 one 1
22 ugte 1 6 21
23 not 1 22
24 implies 1 19 18
25 not 1 24
26 bad 25 ; assert @[d/chiseltest/src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 84:9]
27 implies 1 23 2
28 constraint 27 ; _resetActive
; counter.next
29 zero 3
30 ite 3 2 29 13
31 next 3 4 30
; _resetCount.next
32 sort bitvec 2
33 uext 32 6 1
34 one 1
35 uext 32 34 1
36 add 32 33 35
37 slice 1 36 0 0
38 ite 1 23 37 6
39 next 1 6 38