Skip to content

Commit

Permalink
more bmc tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@ekiwi
ekiwi committed Nov 20, 2023
1 parent 53045ac commit fdd452c
Show file tree
Hide file tree
Showing 6 changed files with 328 additions and 1 deletion.
12 changes: 11 additions & 1 deletion .github/workflows/test.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,10 +46,20 @@ jobs:
run: |
cargo run --release --example bmc -- inputs/Quiz1.btor > Quiz1.wit
btorsim inputs/Quiz1.btor Quiz1.wit
- name: bmc Quiz1 (with additional assumption)
run: |
cargo run --release --example bmc -- inputs/Quiz1.unsat.btor
- name: bmc const array example
run: |
cargo run --release --example bmc -- inputs/const_array_example.btor > const_array_example.wit
btorsim inputs/const_array_example.btor const_array_example.wit
btorsim inputs/const_array_example.btor const_array_example.wit
- name: bmc Quiz2
run: |
cargo run --release --example bmc -- inputs/Quiz2.sat.btor > Quiz2.sat.wit
btorsim inputs/Quiz2.sat.btor Quiz2.sat.wit
- name: bmc Quiz2 (with counter reset value)
run: |
cargo run --release --example bmc -- inputs/Quiz2.unsat.btor
semver:
Expand Down
49 changes: 49 additions & 0 deletions inputs/Quiz1.unsat.btor
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
1 sort bitvec 1
2 input 1 reset
3 sort bitvec 16
4 state 3 counter ; @[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 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 83:22]
13 slice 3 12 15 0 ; @[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 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 84:18]
19 not 1 2 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 84:9]
20 not 1 18 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 84:9]
21 const 14 1001
22 uext 3 21 12
23 ugt 1 4 22
24 not 1 23 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 86:20]
25 not 1 24 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 86:11]
26 one 1
27 ugte 1 6 26
28 not 1 27
29 implies 1 19 18
30 not 1 29
31 bad 30 ; assert @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 84:9]
32 implies 1 19 24
33 constraint 32 ; assume @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 86:11]
34 implies 1 28 2
35 constraint 34 ; _resetActive
; counter.next
36 zero 3
37 ite 3 2 36 13
38 next 3 4 37
; _resetCount.next
39 sort bitvec 2
40 uext 39 6 1
41 one 1
42 uext 39 41 1
43 add 39 40 42
44 slice 1 43 0 0
45 ite 1 28 44 6
46 next 1 6 45
57 changes: 57 additions & 0 deletions inputs/Quiz2.sat.btor
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
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
59 changes: 59 additions & 0 deletions inputs/Quiz2.unsat.btor
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
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 95:40]
; _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 95:40]
29 ite 4 12 19 28 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 98:41 99:13]
30 const 4 0000000000000100
31 ugte 1 5 30
32 not 1 31 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 104:18]
33 not 1 2 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 104:9]
34 not 1 32 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 104:9]
35 one 1
36 ugte 1 7 35
37 not 1 36
38 zero 1
39 uext 4 38 15
40 neq 1 5 39 ; @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 93:17], @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 103:20]
41 implies 1 33 32
42 not 1 41
43 bad 42 ; assert @[src/test/scala/chiseltest/formal/examples/ZipCpuQuizzes.scala 104:9]
44 implies 1 37 2
45 constraint 44 ; _resetActive
; counter.next
46 zero 4
47 ite 4 2 46 29
48 next 4 5 47
; _resetCount.next
49 sort bitvec 2
50 uext 49 7 1
51 one 1
52 uext 49 51 1
53 add 49 50 52
54 slice 1 53 0 0
55 ite 1 37 54 7
56 next 1 7 55
68 changes: 68 additions & 0 deletions inputs/Quiz4.sat.btor
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
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
84 changes: 84 additions & 0 deletions inputs/Quiz4.unsat.btor
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
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

0 comments on commit fdd452c

Please sign in to comment.