Automate SystemVerilog to BTOR conversion for Calyx Primitives (#1757)

* Migrate changes from NgaiJustin/calyx for sv to btor2 conversion

* Update sv2btor.md

docs/tools/sv2btor.md

@@ -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`.
+

tools/btor2/core/std_add.btor

@@ -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

tools/btor2/core/std_and.btor

@@ -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

tools/btor2/core/std_cat.btor

@@ -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

tools/btor2/core/std_eq.btor

@@ -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

tools/btor2/core/std_ge.btor

@@ -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

tools/btor2/core/std_gt.btor

@@ -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

tools/btor2/core/std_le.btor

@@ -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

tools/btor2/core/std_lsh.btor

@@ -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

tools/btor2/core/std_lt.btor

@@ -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

tools/btor2/core/std_mem_d1.btor

@@ -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

tools/btor2/core/std_mem_d2.btor

@@ -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