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