Skip to content

Commit

Permalink
Automate SystemVerilog to BTOR conversion for Calyx Primitives (#1757)
Browse files Browse the repository at this point in the history
* Migrate changes from NgaiJustin/calyx for sv to btor2 conversion

* Update sv2btor.md
  • Loading branch information
NgaiJustin authored and rachitnigam committed Feb 16, 2024
1 parent 77adcc2 commit 89e3e7f
Show file tree
Hide file tree
Showing 27 changed files with 1,453 additions and 0 deletions.
18 changes: 18 additions & 0 deletions docs/tools/sv2btor.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
# `sv2btor`

The `sv2btor` tool is a tool that leverages `yosys` and
`verible` to translate the SystemVerilog files into BTOR2.

# Usage

```bash
Usage: sv2btor.py <PATH_TO_YOSYS_EXECUTABLE> <PATH_TO_VERIBLE_VERILOG_SYNTAX> <OUTPUT_DIR> <VERILOG_FILE [VERILOG_FILE [...]]>
```
# Installation
To run this tool, you need to have `yosys` and `verible-verilog-syntax` installed. You will also need the `anytree` python package.
- You can install `yosys` by following the instructions [here](https://github.com/YosysHQ/yosys).
- You can install `verible-verilog-syntax` by following the instructions [here](https://github.com/chipsalliance/verible). Note that we only need the standalone `verible-verilog-syntax` executable, the rest of the tools are optional.
- You can install `anytree` by running `pip install anytree`.
7 changes: 7 additions & 0 deletions tools/btor2/core/std_add.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_add.
1 sort bitvec 32
2 input 1 left ; temp.sv:5.35-5.39
3 input 1 right ; temp.sv:6.35-6.40
4 add 1 2 3
5 output 4 out ; temp.sv:7.35-7.38
; end of yosys output
7 changes: 7 additions & 0 deletions tools/btor2/core/std_and.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_and.
1 sort bitvec 32
2 input 1 left ; core.sv:97.35-97.39
3 input 1 right ; core.sv:98.35-98.40
4 and 1 2 3
5 output 4 out ; core.sv:99.35-99.38
; end of yosys output
8 changes: 8 additions & 0 deletions tools/btor2/core/std_cat.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_cat.
1 sort bitvec 32
2 input 1 left ; core.sv:63.39-63.43
3 input 1 right ; core.sv:64.40-64.45
4 sort bitvec 64
5 concat 4 2 3
6 output 5 out ; core.sv:65.34-65.37
; end of yosys output
8 changes: 8 additions & 0 deletions tools/btor2/core/std_eq.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_eq.
1 sort bitvec 32
2 input 1 left ; core.sv:157.34-157.38
3 input 1 right ; core.sv:158.34-158.39
4 sort bitvec 1
5 eq 4 2 3
6 output 5 out ; core.sv:159.18-159.21
; end of yosys output
8 changes: 8 additions & 0 deletions tools/btor2/core/std_ge.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_ge.
1 sort bitvec 32
2 input 1 left ; core.sv:177.34-177.38
3 input 1 right ; core.sv:178.34-178.39
4 sort bitvec 1
5 ugte 4 2 3
6 output 5 out ; core.sv:179.18-179.21
; end of yosys output
8 changes: 8 additions & 0 deletions tools/btor2/core/std_gt.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_gt.
1 sort bitvec 32
2 input 1 left ; core.sv:137.34-137.38
3 input 1 right ; core.sv:138.34-138.39
4 sort bitvec 1
5 ugt 4 2 3
6 output 5 out ; core.sv:139.18-139.21
; end of yosys output
8 changes: 8 additions & 0 deletions tools/btor2/core/std_le.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_le.
1 sort bitvec 32
2 input 1 left ; core.sv:187.34-187.38
3 input 1 right ; core.sv:188.34-188.39
4 sort bitvec 1
5 ulte 4 2 3
6 output 5 out ; core.sv:189.18-189.21
; end of yosys output
7 changes: 7 additions & 0 deletions tools/btor2/core/std_lsh.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_lsh.
1 sort bitvec 32
2 input 1 left ; core.sv:197.35-197.39
3 input 1 right ; core.sv:198.35-198.40
4 sll 1 2 3
5 output 4 out ; core.sv:199.35-199.38
; end of yosys output
8 changes: 8 additions & 0 deletions tools/btor2/core/std_lt.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_lt.
1 sort bitvec 32
2 input 1 left ; core.sv:147.34-147.38
3 input 1 right ; core.sv:148.34-148.39
4 sort bitvec 1
5 ult 4 2 3
6 output 5 out ; core.sv:149.18-149.21
; end of yosys output
97 changes: 97 additions & 0 deletions tools/btor2/core/std_mem_d1.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,97 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_mem_d1.
1 sort bitvec 4
2 input 1 addr0 ; core.sv:232.38-232.43
3 sort bitvec 1
4 input 3 clk ; core.sv:235.38-235.41
5 input 3 reset ; core.sv:236.38-236.43
6 sort bitvec 32
7 input 6 write_data ; core.sv:233.38-233.48
8 input 3 write_en ; core.sv:234.38-234.46
9 state 3
10 output 9 done ; core.sv:238.38-238.42
11 sort array 1 6
12 state 11 mem
13 read 6 12 2
14 output 13 read_data ; core.sv:237.38-237.47
15 const 3 0
16 const 3 1
17 ite 3 8 16 15
18 ite 3 5 15 17
19 next 3 9 18
20 input 1
21 not 3 5
22 and 3 21 8
23 ite 1 22 2 20
24 input 6
25 ite 6 22 7 24
26 ite 3 22 16 15
27 sort bitvec 2
28 concat 27 26 26
29 sort bitvec 3
30 concat 29 26 28
31 concat 1 26 30
32 sort bitvec 5
33 concat 32 26 31
34 sort bitvec 6
35 concat 34 26 33
36 sort bitvec 7
37 concat 36 26 35
38 sort bitvec 8
39 concat 38 26 37
40 sort bitvec 9
41 concat 40 26 39
42 sort bitvec 10
43 concat 42 26 41
44 sort bitvec 11
45 concat 44 26 43
46 sort bitvec 12
47 concat 46 26 45
48 sort bitvec 13
49 concat 48 26 47
50 sort bitvec 14
51 concat 50 26 49
52 sort bitvec 15
53 concat 52 26 51
54 sort bitvec 16
55 concat 54 26 53
56 sort bitvec 17
57 concat 56 26 55
58 sort bitvec 18
59 concat 58 26 57
60 sort bitvec 19
61 concat 60 26 59
62 sort bitvec 20
63 concat 62 26 61
64 sort bitvec 21
65 concat 64 26 63
66 sort bitvec 22
67 concat 66 26 65
68 sort bitvec 23
69 concat 68 26 67
70 sort bitvec 24
71 concat 70 26 69
72 sort bitvec 25
73 concat 72 26 71
74 sort bitvec 26
75 concat 74 26 73
76 sort bitvec 27
77 concat 76 26 75
78 sort bitvec 28
79 concat 78 26 77
80 sort bitvec 29
81 concat 80 26 79
82 sort bitvec 30
83 concat 82 26 81
84 sort bitvec 31
85 concat 84 26 83
86 concat 6 26 85
87 read 6 12 23
88 not 6 86
89 and 6 87 88
90 and 6 25 86
91 or 6 90 89
92 write 11 12 23 91
93 redor 3 86
94 ite 11 93 92 12
95 next 11 12 94 mem ; core.sv:241.21-241.24
; end of yosys output
104 changes: 104 additions & 0 deletions tools/btor2/core/std_mem_d2.btor
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_mem_d2.
1 sort bitvec 4
2 input 1 addr0 ; core.sv:272.41-272.46
3 input 1 addr1 ; core.sv:273.41-273.46
4 sort bitvec 1
5 input 4 clk ; core.sv:276.41-276.44
6 input 4 reset ; core.sv:277.41-277.46
7 sort bitvec 32
8 input 7 write_data ; core.sv:274.41-274.51
9 input 4 write_en ; core.sv:275.41-275.49
10 state 4
11 output 10 done ; core.sv:279.41-279.45
12 sort bitvec 8
13 sort array 12 7
14 state 13 mem
15 uext 12 2 4
16 sort bitvec 5
17 const 16 10000
18 uext 12 17 3
19 mul 12 15 18
20 uext 12 3 4
21 add 12 19 20
22 read 7 14 21
23 output 22 read_data ; core.sv:278.41-278.50
24 const 4 0
25 const 4 1
26 ite 4 9 25 24
27 ite 4 6 24 26
28 next 4 10 27
29 input 12
30 not 4 6
31 and 4 30 9
32 ite 12 31 21 29
33 input 7
34 ite 7 31 8 33
35 ite 4 31 25 24
36 sort bitvec 2
37 concat 36 35 35
38 sort bitvec 3
39 concat 38 35 37
40 concat 1 35 39
41 concat 16 35 40
42 sort bitvec 6
43 concat 42 35 41
44 sort bitvec 7
45 concat 44 35 43
46 concat 12 35 45
47 sort bitvec 9
48 concat 47 35 46
49 sort bitvec 10
50 concat 49 35 48
51 sort bitvec 11
52 concat 51 35 50
53 sort bitvec 12
54 concat 53 35 52
55 sort bitvec 13
56 concat 55 35 54
57 sort bitvec 14
58 concat 57 35 56
59 sort bitvec 15
60 concat 59 35 58
61 sort bitvec 16
62 concat 61 35 60
63 sort bitvec 17
64 concat 63 35 62
65 sort bitvec 18
66 concat 65 35 64
67 sort bitvec 19
68 concat 67 35 66
69 sort bitvec 20
70 concat 69 35 68
71 sort bitvec 21
72 concat 71 35 70
73 sort bitvec 22
74 concat 73 35 72
75 sort bitvec 23
76 concat 75 35 74
77 sort bitvec 24
78 concat 77 35 76
79 sort bitvec 25
80 concat 79 35 78
81 sort bitvec 26
82 concat 81 35 80
83 sort bitvec 27
84 concat 83 35 82
85 sort bitvec 28
86 concat 85 35 84
87 sort bitvec 29
88 concat 87 35 86
89 sort bitvec 30
90 concat 89 35 88
91 sort bitvec 31
92 concat 91 35 90
93 concat 7 35 92
94 read 7 14 32
95 not 7 93
96 and 7 94 95
97 and 7 34 93
98 or 7 97 96
99 write 13 14 32 98
100 redor 4 93
101 ite 13 100 99 14
102 next 13 14 101 mem ; core.sv:283.21-283.24
; end of yosys output
Loading

0 comments on commit 89e3e7f

Please sign in to comment.