diff --git a/.testall.sh b/.testall.sh index 7fe681f..e74b507 100644 --- a/.testall.sh +++ b/.testall.sh @@ -1,6 +1,8 @@ python generate_test.py python generate_mac.py +python generate_axmuls.py cd tests bash test_mac.sh bash test_circuits.sh +bash test_circuits_verilog.sh bash test_circuits_cgp.sh \ No newline at end of file diff --git a/README.md b/README.md index 067f629..0ade3af 100644 --- a/README.md +++ b/README.md @@ -4,11 +4,11 @@ ## Description -ArithsGen presents an open source tool that enables generation of various arithmetic circuits along with the possibility to export them to various representations which all serve their specific purpose. C language for easy simulation, Verilog for logic synthesis, BLIF for formal verification possibilities and CGP to enable further global optimization. +ArithsGen presents an open source tool that enables generation of various arithmetic circuits along with the possibility to export them to various formats which all serve their specific purpose. C language for easy simulation, Verilog for logic synthesis, BLIF for formal verification possibilities and CGP to enable further global optimization. In contrast to standard HDL languages Python supports -* Multiple output formats (BLIF, Verilog, C, Integer netlis) -* Advanced langugage construction (better configuration, inheritance, etc.) +* Multiple output formats (BLIF, Verilog, C, Integer netlist) +* Advanced language construction (better configuration, inheritance, etc.) * Support of various PDKs (for using library cells as half-adders and full-adders) ## Prebuild circuits @@ -81,13 +81,13 @@ You can add a support of arbitrary PDK (see an [example](ariths_gen/pdk.py) ). ## Approximate circuits -Besides the accurate arithmetic circuits you can generate some approximate circuits. Currently we support _Broken Array Multiplier_ and _Truncated Multiplier_. For more details please follow files in folder [approximate_multipliers](ariths_gen/multi_bit_circuits/approximate_multipliers/). You can simply run +Besides the accurate arithmetic circuits you can generate some approximate circuits. Currently we support _Broken Array Multiplier_ and _Truncated Multiplier_ both with fully connected architectures composed from half/full adders as well as faster implementations using carry save multiplier. For more details please follow files in folder [approximate_multipliers](ariths_gen/multi_bit_circuits/approximate_multipliers/). You can simply run ```bash python3 generate_axmuls.py ``` to get the approximate circuits. -The module also supports evaluation of the proposed circuits. You can call the instation as a function (even with numpy-array input) to obtain the results of multiplication operation +The module also supports evaluation of the proposed circuits. You can call the instation as a function (even with numpy-array input) to obtain the results of multiplication operation. ```py from ariths_gen.wire_components.buses import Bus @@ -124,7 +124,7 @@ print("Mean average error", np.abs(r - (va * vb)).mean()) ## Formal verification The `yosys_equiv_check.sh` script enables to formally check the equivalence of generated Verilog and BLIF representations of the same circuit. -It uses the Yosys Open SYnthesis Suite tool by Clifford Wolf. For further information, please visit: http://www.clifford.at/yosys/documentation.html. +It uses the Yosys Open SYnthesis Suite tool by Claire Xenia Wolf. For further information, please visit: http://bygone.clairexen.net/yosys/documentation.html. ## Execute permission ```bash @@ -133,7 +133,7 @@ chmod +x yosys_equiv_check.sh ### Usage ```bash -./yosys_equiv_check.sh -v "verilog_file" -b "blif_file" [-H] +./yosys_equiv_check.sh -v "verilog_file" -b "blif_file" -m "method" [-H] ``` For more detailed description of script's usage, use help. diff --git a/generate_axmuls.py b/generate_axmuls.py index d77524b..f8345fe 100644 --- a/generate_axmuls.py +++ b/generate_axmuls.py @@ -6,9 +6,18 @@ from ariths_gen.wire_components import ( Bus ) +from ariths_gen.multi_bit_circuits.adders import ( + UnsignedCarryLookaheadAdder, + UnsignedPGRippleCarryAdder, + UnsignedRippleCarryAdder, + UnsignedCarrySkipAdder, +) + from ariths_gen.multi_bit_circuits.approximate_multipliers import ( - UnsignedTruncatedMultiplier, - UnsignedBrokenArrayMultiplier + UnsignedTruncatedArrayMultiplier, + UnsignedTruncatedCarrySaveMultiplier, + UnsignedBrokenArrayMultiplier, + UnsignedBrokenCarrySaveMultiplier ) from ariths_gen.pdk import * @@ -27,6 +36,8 @@ if __name__ == "__main__": # 8-bit unsigned BAMs root_path = "test_circuits/ax" + + adders = {UnsignedCarryLookaheadAdder: "cla", UnsignedPGRippleCarryAdder: "pg_rca", UnsignedRippleCarryAdder: "rca", UnsignedCarrySkipAdder: "cska"} i = 0 for h in range(0, 8): @@ -36,25 +47,47 @@ if __name__ == "__main__": N=8 a = Bus(prefix="a", N=N) b = Bus(prefix="b", N=N) - - u_bam = UnsignedBrokenArrayMultiplier(a, b, name=f"f_u_bam{N}_h{h}_v{v}", horizontal_cut=h, vertical_cut=v) - u_bam.get_c_code_flat(open_file_with_folder(os.path.join(root_path, f"BAM/C/flat/f_u_bam{N}_h{h}_v{v}.c"), "w")) - u_bam.get_v_code_flat(open_file_with_folder(os.path.join(root_path, f"BAM/Verilog/flat/f_u_bam{N}_h{h}_v{v}.v"), "w")) - - u_bam = UnsignedBrokenArrayMultiplier(a, b, name=f"h_u_bam{N}_h{h}_v{v}", horizontal_cut=h, vertical_cut=v) - u_bam.get_c_code_hier(open_file_with_folder(os.path.join(root_path, f"BAM/C/hier/h_u_bam{N}_h{h}_v{v}.c"), "w")) - u_bam.get_v_code_hier(open_file_with_folder(os.path.join(root_path, f"BAM/Verilog/hier/h_u_bam{N}_h{h}_v{v}.v"), "w")) + + for bam in [UnsignedBrokenArrayMultiplier, UnsignedBrokenCarrySaveMultiplier]: + if bam == UnsignedBrokenCarrySaveMultiplier: + for add_type in adders.keys(): + flat_bam = bam(a, b, name=f"f_u_csabam{N}_{adders[add_type]}_h{h}_v{v}", horizontal_cut=h, vertical_cut=v, unsigned_adder_class_name=add_type) + hier_bam = bam(a, b, name=f"h_u_csabam{N}_{adders[add_type]}_h{h}_v{v}", horizontal_cut=h, vertical_cut=v, unsigned_adder_class_name=add_type) + flat_bam.get_c_code_flat(open_file_with_folder(os.path.join(root_path, f"BAM/C/flat/f_u_csabam{N}_{adders[add_type]}_h{h}_v{v}.c"), "w")) + flat_bam.get_v_code_flat(open_file_with_folder(os.path.join(root_path, f"BAM/Verilog/flat/f_u_csabam{N}_{adders[add_type]}_h{h}_v{v}.v"), "w")) + hier_bam.get_c_code_hier(open_file_with_folder(os.path.join(root_path, f"BAM/C/hier/h_u_csabam{N}_{adders[add_type]}_h{h}_v{v}.c"), "w")) + hier_bam.get_v_code_hier(open_file_with_folder(os.path.join(root_path, f"BAM/Verilog/hier/h_u_csabam{N}_{adders[add_type]}_h{h}_v{v}.v"), "w")) + else: + flat_bam = bam(a, b, name=f"f_u_arrbam{N}_h{h}_v{v}", horizontal_cut=h, vertical_cut=v) + hier_bam = bam(a, b, name=f"h_u_arrbam{N}_h{h}_v{v}", horizontal_cut=h, vertical_cut=v) + + flat_bam.get_c_code_flat(open_file_with_folder(os.path.join(root_path, f"BAM/C/flat/f_u_arrbam{N}_h{h}_v{v}.c"), "w")) + flat_bam.get_v_code_flat(open_file_with_folder(os.path.join(root_path, f"BAM/Verilog/flat/f_u_arrbam{N}_h{h}_v{v}.v"), "w")) + hier_bam.get_c_code_hier(open_file_with_folder(os.path.join(root_path, f"BAM/C/hier/h_u_arrbam{N}_h{h}_v{v}.c"), "w")) + hier_bam.get_v_code_hier(open_file_with_folder(os.path.join(root_path, f"BAM/Verilog/hier/h_u_arrbam{N}_h{h}_v{v}.v"), "w")) + # 8-bit unsigned TMs for i in range(0, 8): N=8 a = Bus(prefix="a", N=N) b = Bus(prefix="b", N=N) - - u_tm = UnsignedTruncatedMultiplier(a, b, name=f"f_u_tm{N}_k{i}", truncation_cut=i) - u_tm.get_c_code_flat(open_file_with_folder(os.path.join(root_path, f"TM/C/flat/f_u_tm{N}_k{i}.c"), "w")) - u_tm.get_v_code_flat(open_file_with_folder(os.path.join(root_path, f"TM/Verilog/flat/f_u_tm{N}_k{i}.v"), "w")) - - u_tm = UnsignedTruncatedMultiplier(a, b, name=f"h_u_tm{N}_k{i}", truncation_cut=i) - u_tm.get_c_code_hier(open_file_with_folder(os.path.join(root_path, f"TM/C/hier/h_u_tm{N}_k{i}.c"), "w")) - u_tm.get_v_code_hier(open_file_with_folder(os.path.join(root_path, f"TM/Verilog/hier/h_u_tm{N}_k{i}.v"), "w")) + + for tm in [UnsignedTruncatedArrayMultiplier, UnsignedTruncatedCarrySaveMultiplier]: + if tm == UnsignedTruncatedCarrySaveMultiplier: + for add_type in adders.keys(): + flat_tm = tm(a, b, name=f"f_u_csatm{N}_{adders[add_type]}_k{i}", truncation_cut=i, unsigned_adder_class_name=add_type) + hier_tm = tm(a, b, name=f"h_u_csatm{N}_{adders[add_type]}_k{i}", truncation_cut=i, unsigned_adder_class_name=add_type) + + flat_tm.get_c_code_flat(open_file_with_folder(os.path.join(root_path, f"TM/C/flat/f_u_csatm{N}_{adders[add_type]}_k{i}.c"), "w")) + flat_tm.get_v_code_flat(open_file_with_folder(os.path.join(root_path, f"TM/Verilog/flat/f_u_csatm{N}_{adders[add_type]}_k{i}.v"), "w")) + hier_tm.get_c_code_hier(open_file_with_folder(os.path.join(root_path, f"TM/C/hier/h_u_csatm{N}_{adders[add_type]}_k{i}.c"), "w")) + hier_tm.get_v_code_hier(open_file_with_folder(os.path.join(root_path, f"TM/Verilog/hier/h_u_csatm{N}_{adders[add_type]}_k{i}.v"), "w")) + else: + flat_tm = tm(a, b, name=f"f_u_arrtm{N}_k{i}", truncation_cut=i) + hier_tm = tm(a, b, name=f"h_u_arrtm{N}_k{i}", truncation_cut=i) + + flat_tm.get_c_code_flat(open_file_with_folder(os.path.join(root_path, f"TM/C/flat/f_u_arrtm{N}_k{i}.c"), "w")) + flat_tm.get_v_code_flat(open_file_with_folder(os.path.join(root_path, f"TM/Verilog/flat/f_u_arrtm{N}_k{i}.v"), "w")) + hier_tm.get_c_code_hier(open_file_with_folder(os.path.join(root_path, f"TM/C/hier/h_u_arrtm{N}_k{i}.c"), "w")) + hier_tm.get_v_code_hier(open_file_with_folder(os.path.join(root_path, f"TM/Verilog/hier/h_u_arrtm{N}_k{i}.v"), "w")) diff --git a/generate_test.py b/generate_test.py index 85f2c21..6fc733a 100644 --- a/generate_test.py +++ b/generate_test.py @@ -40,9 +40,11 @@ from ariths_gen.multi_bit_circuits.multipliers import ( UnsignedDaddaMultiplier, UnsignedArrayMultiplier, UnsignedWallaceMultiplier, + UnsignedCarrySaveMultiplier, SignedArrayMultiplier, SignedDaddaMultiplier, SignedWallaceMultiplier, + SignedCarrySaveMultiplier ) from ariths_gen.multi_bit_circuits.dividers import ( @@ -56,6 +58,7 @@ def prepare_directory(path): os.makedirs(os.path.dirname(path), exist_ok=True) return open(path, "w") + def export_circuit(circuit, name): directory = "test_circuits" @@ -78,6 +81,7 @@ if __name__ == "__main__": representation = "h" + """ ADDERS """ # RCA name = f"u_rca{N}" circuit = UnsignedRippleCarryAdder(a, b, name=name) @@ -114,6 +118,7 @@ if __name__ == "__main__": circuit = SignedCarryLookaheadAdder(a, b, name=name) export_circuit(circuit, name) + """ MULTIPLIERS """ # Arrmul name = f"u_arrmul{N}" circuit = UnsignedArrayMultiplier(a, b, name=name) @@ -123,40 +128,106 @@ if __name__ == "__main__": circuit = SignedArrayMultiplier(a, b, name=name) export_circuit(circuit, name) - # Wallace + # Csamul (Braun multiplier) + name = f"u_csamul_cla{N}" + circuit = UnsignedCarrySaveMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarryLookaheadAdder) + export_circuit(circuit, name) + + name = f"s_csamul_cla{N}" + circuit = SignedCarrySaveMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarryLookaheadAdder) + export_circuit(circuit, name) + + name = f"u_csamul_rca{N}" + circuit = UnsignedCarrySaveMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedRippleCarryAdder) + export_circuit(circuit, name) + + name = f"s_csamul_rca{N}" + circuit = SignedCarrySaveMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedRippleCarryAdder) + export_circuit(circuit, name) + + name = f"u_csamul_pg_rca{N}" + circuit = UnsignedCarrySaveMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedPGRippleCarryAdder) + export_circuit(circuit, name) + + name = f"s_csamul_pg_rca{N}" + circuit = SignedCarrySaveMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedPGRippleCarryAdder) + export_circuit(circuit, name) + + name = f"u_csamul_cska{N}" + circuit = UnsignedCarrySaveMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarrySkipAdder) + export_circuit(circuit, name) + + name = f"s_csamul_cska{N}" + circuit = SignedCarrySaveMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarrySkipAdder) + export_circuit(circuit, name) + + # Wallace implemented with interconnected HAs/FAs name = f"u_wallace_cla{N}" - circuit = UnsignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarryLookaheadAdder) + circuit = UnsignedWallaceMultiplier(a, b, name=name, use_csa=False, unsigned_adder_class_name=UnsignedCarryLookaheadAdder) export_circuit(circuit, name) name = f"s_wallace_cla{N}" - circuit = SignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarryLookaheadAdder) + circuit = SignedWallaceMultiplier(a, b, name=name, use_csa=False, unsigned_adder_class_name=UnsignedCarryLookaheadAdder) export_circuit(circuit, name) name = f"u_wallace_rca{N}" - circuit = UnsignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedRippleCarryAdder) + circuit = UnsignedWallaceMultiplier(a, b, name=name, use_csa=False, unsigned_adder_class_name=UnsignedRippleCarryAdder) export_circuit(circuit, name) name = f"s_wallace_rca{N}" - circuit = SignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedRippleCarryAdder) + circuit = SignedWallaceMultiplier(a, b, name=name, use_csa=False, unsigned_adder_class_name=UnsignedRippleCarryAdder) export_circuit(circuit, name) name = f"u_wallace_pg_rca{N}" - circuit = UnsignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedPGRippleCarryAdder) + circuit = UnsignedWallaceMultiplier(a, b, name=name, use_csa=False, unsigned_adder_class_name=UnsignedPGRippleCarryAdder) export_circuit(circuit, name) name = f"s_wallace_pg_rca{N}" - circuit = SignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedPGRippleCarryAdder) + circuit = SignedWallaceMultiplier(a, b, name=name, use_csa=False, unsigned_adder_class_name=UnsignedPGRippleCarryAdder) export_circuit(circuit, name) name = f"u_wallace_cska{N}" - circuit = UnsignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarrySkipAdder) + circuit = UnsignedWallaceMultiplier(a, b, name=name, use_csa=False, unsigned_adder_class_name=UnsignedCarrySkipAdder) export_circuit(circuit, name) name = f"s_wallace_cska{N}" + circuit = SignedWallaceMultiplier(a, b, name=name, use_csa=False, unsigned_adder_class_name=UnsignedCarrySkipAdder) + export_circuit(circuit, name) + + # Wallace implemented with interconnected CSAs (default choice) + name = f"u_CSAwallace_cla{N}" + circuit = UnsignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarryLookaheadAdder) + export_circuit(circuit, name) + + name = f"s_CSAwallace_cla{N}" + circuit = SignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarryLookaheadAdder) + export_circuit(circuit, name) + + name = f"u_CSAwallace_rca{N}" + circuit = UnsignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedRippleCarryAdder) + export_circuit(circuit, name) + + name = f"s_CSAwallace_rca{N}" + circuit = SignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedRippleCarryAdder) + export_circuit(circuit, name) + + name = f"u_CSAwallace_pg_rca{N}" + circuit = UnsignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedPGRippleCarryAdder) + export_circuit(circuit, name) + + name = f"s_CSAwallace_pg_rca{N}" + circuit = SignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedPGRippleCarryAdder) + export_circuit(circuit, name) + + name = f"u_CSAwallace_cska{N}" + circuit = UnsignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarrySkipAdder) + export_circuit(circuit, name) + + name = f"s_CSAwallace_cska{N}" circuit = SignedWallaceMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarrySkipAdder) export_circuit(circuit, name) - # Dadda + # Dadda with interconnected HAs/FAs name = f"u_dadda_cla{N}" circuit = UnsignedDaddaMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarryLookaheadAdder) export_circuit(circuit, name) @@ -189,6 +260,7 @@ if __name__ == "__main__": circuit = SignedDaddaMultiplier(a, b, name=name, unsigned_adder_class_name=UnsignedCarrySkipAdder) export_circuit(circuit, name) + """ DIVIDERS """ # Arrdiv name = f"arrdiv{N}" circuit = ArrayDivider(a, b, name=name) diff --git a/tests/test_all.py b/tests/test_all.py index 30ebb24..5bb9f46 100644 --- a/tests/test_all.py +++ b/tests/test_all.py @@ -22,16 +22,18 @@ from ariths_gen.multi_bit_circuits.multipliers import ( UnsignedDaddaMultiplier, UnsignedArrayMultiplier, UnsignedWallaceMultiplier, + UnsignedCarrySaveMultiplier, SignedArrayMultiplier, SignedDaddaMultiplier, SignedWallaceMultiplier, + SignedCarrySaveMultiplier ) from ariths_gen.multi_bit_circuits.approximate_multipliers import ( - UnsignedTruncatedMultiplier, - SignedTruncatedMultiplier, + UnsignedTruncatedArrayMultiplier, + UnsignedTruncatedCarrySaveMultiplier, UnsignedBrokenArrayMultiplier, - SignedBrokenArrayMultiplier + UnsignedBrokenCarrySaveMultiplier ) import numpy as np @@ -45,10 +47,10 @@ def test_unsigned_approxmul(values = False): bv = av.reshape(-1, 1) expected = av * bv - for c in [UnsignedBrokenArrayMultiplier, UnsignedTruncatedMultiplier]: - if c == UnsignedTruncatedMultiplier: + for c in [UnsignedBrokenArrayMultiplier, UnsignedBrokenCarrySaveMultiplier, UnsignedTruncatedArrayMultiplier, UnsignedTruncatedCarrySaveMultiplier]: + if c == UnsignedTruncatedArrayMultiplier or c == UnsignedTruncatedCarrySaveMultiplier: mul = c(a=a, b=b, truncation_cut=2) - elif c == UnsignedBrokenArrayMultiplier: + elif c == UnsignedBrokenArrayMultiplier or c == UnsignedBrokenCarrySaveMultiplier: mul = c(a=a, b=b, horizontal_cut=1, vertical_cut=2) r = mul(av, bv) @@ -59,10 +61,10 @@ def test_unsigned_approxmul(values = False): np.seterr(divide='ignore', invalid='ignore') WCRE = np.max(np.nan_to_num(abs(np.subtract(r, expected)) / expected)) - if isinstance(mul, UnsignedTruncatedMultiplier): + if isinstance(mul, UnsignedTruncatedArrayMultiplier) or isinstance(mul, UnsignedTruncatedCarrySaveMultiplier): # WCE_TM(n,k) = (2^k - 1) * (2^(n+1) - 2^k - 1) expected_WCE = (2 ** mul.truncation_cut - 1) * (2 ** (mul.a.N+1) - 2 ** mul.truncation_cut - 1) - elif isinstance(mul, UnsignedBrokenArrayMultiplier): + elif isinstance(mul, UnsignedBrokenArrayMultiplier) or isinstance(mul, UnsignedBrokenCarrySaveMultiplier): # WCE_BAM(n,h,v) = (2^n - 1) * {SUM_i0_to_h-1}(2^i) + 2^h * {SUM_i0_to_v-h-1}(2^(v-h) - 2^i) sum_1 = sum([2**i for i in range(0, mul.horizontal_cut)]) sum_2 = sum([2**(mul.vertical_cut-mul.horizontal_cut) - 2**i for i in range(0, mul.vertical_cut-mul.horizontal_cut)]) @@ -82,11 +84,16 @@ def test_unsigned_mul(): bv = av.reshape(-1, 1) expected = av * bv - for c in [UnsignedDaddaMultiplier, UnsignedArrayMultiplier, UnsignedWallaceMultiplier]: + for c in [UnsignedDaddaMultiplier, UnsignedArrayMultiplier, UnsignedCarrySaveMultiplier, UnsignedWallaceMultiplier]: mul = c(a, b) assert mul(0, 0) == 0 r = mul(av, bv) np.testing.assert_array_equal(expected, r) + # For array wallace tree implementation + mul = UnsignedWallaceMultiplier(a, b, use_csa=False) + assert mul(0, 0) == 0 + r = mul(av, bv) + np.testing.assert_array_equal(expected, r) def test_signed_mul(): """ Test signed multipliers """ @@ -97,11 +104,16 @@ def test_signed_mul(): bv = av.reshape(-1, 1) expected = av * bv - for c in [SignedDaddaMultiplier, SignedArrayMultiplier, SignedWallaceMultiplier]: + for c in [SignedDaddaMultiplier, SignedArrayMultiplier, SignedWallaceMultiplier, SignedCarrySaveMultiplier]: mul = c(a, b) r = mul(av, bv) assert mul(0, 0) == 0 np.testing.assert_array_equal(expected, r) + # For array wallace tree implementation + mul = SignedWallaceMultiplier(a, b, use_csa=False) + r = mul(av, bv) + assert mul(0, 0) == 0 + np.testing.assert_array_equal(expected, r) def test_unsigned_add(): """ Test unsigned adders """ diff --git a/tests/test_cgp.py b/tests/test_cgp.py index 5c9abf1..59876ff 100644 --- a/tests/test_cgp.py +++ b/tests/test_cgp.py @@ -22,20 +22,22 @@ from ariths_gen.multi_bit_circuits.multipliers import ( UnsignedDaddaMultiplier, UnsignedArrayMultiplier, UnsignedWallaceMultiplier, + UnsignedCarrySaveMultiplier, SignedArrayMultiplier, SignedDaddaMultiplier, SignedWallaceMultiplier, + SignedCarrySaveMultiplier ) from ariths_gen.multi_bit_circuits.approximate_multipliers import ( - UnsignedTruncatedMultiplier, - SignedTruncatedMultiplier, + UnsignedTruncatedArrayMultiplier, + UnsignedTruncatedCarrySaveMultiplier, UnsignedBrokenArrayMultiplier, - SignedBrokenArrayMultiplier + UnsignedBrokenCarrySaveMultiplier ) -from ariths_gen.multi_bit_circuits.cgp_circuit import UnsignedCGPCircuit, SignedCGPCircuit +from ariths_gen.core.cgp_circuit import UnsignedCGPCircuit, SignedCGPCircuit import numpy as np from io import StringIO @@ -106,7 +108,7 @@ def test_unsigned_mul(): bv = av.reshape(-1, 1) expected = av * bv - for c in [UnsignedDaddaMultiplier, UnsignedArrayMultiplier, UnsignedWallaceMultiplier]: + for c in [UnsignedDaddaMultiplier, UnsignedArrayMultiplier, UnsignedCarrySaveMultiplier, UnsignedWallaceMultiplier]: mul = c(a, b) code = StringIO() mul.get_cgp_code_flat(code) @@ -126,7 +128,7 @@ def test_signed_mul(): bv = av.reshape(-1, 1) expected = av * bv - for c in [SignedDaddaMultiplier, SignedArrayMultiplier, SignedWallaceMultiplier]: + for c in [SignedDaddaMultiplier, SignedArrayMultiplier, SignedWallaceMultiplier, SignedCarrySaveMultiplier]: mul = c(a, b) code = StringIO() mul.get_cgp_code_flat(code) diff --git a/tests/test_circuits.sh b/tests/test_circuits.sh index 1ea48ed..5d1d91a 100755 --- a/tests/test_circuits.sh +++ b/tests/test_circuits.sh @@ -34,22 +34,38 @@ test_circuit "adder_unsigned" "u_cska8" test_circuit "adder_unsigned" "u_cla8" -test_circuit "multiplier_signed" "s_arrmul8" +test_circuit "multiplier_signed" "s_arrmul8" +test_circuit "multiplier_signed" "s_csamul_cla8" +test_circuit "multiplier_signed" "s_csamul_rca8" +test_circuit "multiplier_signed" "s_csamul_pg_rca8" +test_circuit "multiplier_signed" "s_csamul_cska8" test_circuit "multiplier_signed" "s_wallace_cla8" test_circuit "multiplier_signed" "s_wallace_rca8" test_circuit "multiplier_signed" "s_wallace_pg_rca8" test_circuit "multiplier_signed" "s_wallace_cska8" +test_circuit "multiplier_signed" "s_CSAwallace_cla8" +test_circuit "multiplier_signed" "s_CSAwallace_rca8" +test_circuit "multiplier_signed" "s_CSAwallace_pg_rca8" +test_circuit "multiplier_signed" "s_CSAwallace_cska8" test_circuit "multiplier_signed" "s_dadda_cla8" test_circuit "multiplier_signed" "s_dadda_rca8" test_circuit "multiplier_signed" "s_dadda_pg_rca8" test_circuit "multiplier_signed" "s_dadda_cska8" -test_circuit "multiplier_unsigned" "u_arrmul8" +test_circuit "multiplier_unsigned" "u_arrmul8" +test_circuit "multiplier_unsigned" "u_csamul_cla8" +test_circuit "multiplier_unsigned" "u_csamul_rca8" +test_circuit "multiplier_unsigned" "u_csamul_pg_rca8" +test_circuit "multiplier_unsigned" "u_csamul_cska8" test_circuit "multiplier_unsigned" "u_wallace_cla8" test_circuit "multiplier_unsigned" "u_wallace_rca8" test_circuit "multiplier_unsigned" "u_wallace_pg_rca8" -test_circuit "multiplier_unsigned" "u_wallace_cska8" +test_circuit "multiplier_unsigned" "u_wallace_cska8" +test_circuit "multiplier_unsigned" "u_CSAwallace_cla8" +test_circuit "multiplier_unsigned" "u_CSAwallace_rca8" +test_circuit "multiplier_unsigned" "u_CSAwallace_pg_rca8" +test_circuit "multiplier_unsigned" "u_CSAwallace_cska8" test_circuit "multiplier_unsigned" "u_dadda_cla8" test_circuit "multiplier_unsigned" "u_dadda_rca8" test_circuit "multiplier_unsigned" "u_dadda_pg_rca8" @@ -71,10 +87,18 @@ fi # exporting s_cska8 # exporting s_cla8 # exporting s_arrmul8 +# exporting s_csamul_cla8 +# exporting s_csamul_rca8 +# exporting s_csamul_pg_rca8 +# exporting s_csamul_cska8 # exporting s_wallace_cla8 # exporting s_wallace_rca8 # exporting s_wallace_pg_rca8 # exporting s_wallace_cska8 +# exporting s_CSAwallace_cla8 +# exporting s_CSAwallace_rca8 +# exporting s_CSAwallace_pg_rca8 +# exporting s_CSAwallace_cska8 # exporting s_dadda_cla8 # exporting s_dadda_rca8 # exporting s_dadda_pg_rca8 @@ -84,10 +108,18 @@ fi # exporting u_cska8 # exporting u_cla8 # exporting u_arrmul8 +# exporting u_csamul_cla8 +# exporting u_csamul_rca8 +# exporting u_csamul_pg_rca8 +# exporting u_csamul_cska8 # exporting u_wallace_cla8 # exporting u_wallace_rca8 # exporting u_wallace_pg_rca8 # exporting u_wallace_cska8 +# exporting u_CSAwallace_pg_rca8 +# exporting u_CSAwallace_rca8 +# exporting u_CSAwallace_cla8 +# exporting u_CSAwallace_cska8 # exporting u_dadda_cla8 # exporting u_dadda_rca8 # exporting u_dadda_pg_rca8 diff --git a/tests/test_circuits_cgp.sh b/tests/test_circuits_cgp.sh index 1002f31..a4dcf03 100755 --- a/tests/test_circuits_cgp.sh +++ b/tests/test_circuits_cgp.sh @@ -39,22 +39,38 @@ test_circuit "adder_unsigned" "u_cska8" test_circuit "adder_unsigned" "u_cla8" -test_circuit "multiplier_signed" "s_arrmul8" +test_circuit "multiplier_signed" "s_arrmul8" +test_circuit "multiplier_signed" "s_csamul_cla8" +test_circuit "multiplier_signed" "s_csamul_rca8" +test_circuit "multiplier_signed" "s_csamul_pg_rca8" +test_circuit "multiplier_signed" "s_csamul_cska8" test_circuit "multiplier_signed" "s_wallace_cla8" test_circuit "multiplier_signed" "s_wallace_rca8" test_circuit "multiplier_signed" "s_wallace_pg_rca8" test_circuit "multiplier_signed" "s_wallace_cska8" +test_circuit "multiplier_signed" "s_CSAwallace_cla8" +test_circuit "multiplier_signed" "s_CSAwallace_rca8" +test_circuit "multiplier_signed" "s_CSAwallace_pg_rca8" +test_circuit "multiplier_signed" "s_CSAwallace_cska8" test_circuit "multiplier_signed" "s_dadda_cla8" test_circuit "multiplier_signed" "s_dadda_rca8" test_circuit "multiplier_signed" "s_dadda_pg_rca8" test_circuit "multiplier_signed" "s_dadda_cska8" -test_circuit "multiplier_unsigned" "u_arrmul8" +test_circuit "multiplier_unsigned" "u_arrmul8" +test_circuit "multiplier_unsigned" "u_csamul_cla8" +test_circuit "multiplier_unsigned" "u_csamul_rca8" +test_circuit "multiplier_unsigned" "u_csamul_pg_rca8" +test_circuit "multiplier_unsigned" "u_csamul_cska8" test_circuit "multiplier_unsigned" "u_wallace_cla8" test_circuit "multiplier_unsigned" "u_wallace_rca8" test_circuit "multiplier_unsigned" "u_wallace_pg_rca8" -test_circuit "multiplier_unsigned" "u_wallace_cska8" +test_circuit "multiplier_unsigned" "u_wallace_cska8" +test_circuit "multiplier_unsigned" "u_CSAwallace_cla8" +test_circuit "multiplier_unsigned" "u_CSAwallace_rca8" +test_circuit "multiplier_unsigned" "u_CSAwallace_pg_rca8" +test_circuit "multiplier_unsigned" "u_CSAwallace_cska8" test_circuit "multiplier_unsigned" "u_dadda_cla8" test_circuit "multiplier_unsigned" "u_dadda_rca8" test_circuit "multiplier_unsigned" "u_dadda_pg_rca8" @@ -76,10 +92,18 @@ fi # exporting s_cska8 # exporting s_cla8 # exporting s_arrmul8 +# exporting s_csamul_cla8 +# exporting s_csamul_rca8 +# exporting s_csamul_pg_rca8 +# exporting s_csamul_cska8 # exporting s_wallace_cla8 # exporting s_wallace_rca8 # exporting s_wallace_pg_rca8 # exporting s_wallace_cska8 +# exporting s_CSAwallace_cla8 +# exporting s_CSAwallace_rca8 +# exporting s_CSAwallace_pg_rca8 +# exporting s_CSAwallace_cska8 # exporting s_dadda_cla8 # exporting s_dadda_rca8 # exporting s_dadda_pg_rca8 @@ -89,10 +113,18 @@ fi # exporting u_cska8 # exporting u_cla8 # exporting u_arrmul8 +# exporting u_csamul_cla8 +# exporting u_csamul_rca8 +# exporting u_csamul_pg_rca8 +# exporting u_csamul_cska8 # exporting u_wallace_cla8 # exporting u_wallace_rca8 # exporting u_wallace_pg_rca8 # exporting u_wallace_cska8 +# exporting u_CSAwallace_pg_rca8 +# exporting u_CSAwallace_rca8 +# exporting u_CSAwallace_cla8 +# exporting u_CSAwallace_cska8 # exporting u_dadda_cla8 # exporting u_dadda_rca8 # exporting u_dadda_pg_rca8 diff --git a/tests/test_circuits_verilog.sh b/tests/test_circuits_verilog.sh index 9617e69..3f72298 100644 --- a/tests/test_circuits_verilog.sh +++ b/tests/test_circuits_verilog.sh @@ -47,22 +47,38 @@ test_circuit "adder_unsigned" "u_cska8" test_circuit "adder_unsigned" "u_cla8" -test_circuit "multiplier_signed" "s_arrmul8" +test_circuit "multiplier_signed" "s_arrmul8" +test_circuit "multiplier_signed" "s_csamul_cla8" +test_circuit "multiplier_signed" "s_csamul_rca8" +test_circuit "multiplier_signed" "s_csamul_pg_rca8" +test_circuit "multiplier_signed" "s_csamul_cska8" test_circuit "multiplier_signed" "s_wallace_cla8" test_circuit "multiplier_signed" "s_wallace_rca8" test_circuit "multiplier_signed" "s_wallace_pg_rca8" test_circuit "multiplier_signed" "s_wallace_cska8" +test_circuit "multiplier_signed" "s_CSAwallace_cla8" +test_circuit "multiplier_signed" "s_CSAwallace_rca8" +test_circuit "multiplier_signed" "s_CSAwallace_pg_rca8" +test_circuit "multiplier_signed" "s_CSAwallace_cska8" test_circuit "multiplier_signed" "s_dadda_cla8" test_circuit "multiplier_signed" "s_dadda_rca8" test_circuit "multiplier_signed" "s_dadda_pg_rca8" test_circuit "multiplier_signed" "s_dadda_cska8" -test_circuit "multiplier_unsigned" "u_arrmul8" +test_circuit "multiplier_unsigned" "u_arrmul8" +test_circuit "multiplier_unsigned" "u_csamul_cla8" +test_circuit "multiplier_unsigned" "u_csamul_rca8" +test_circuit "multiplier_unsigned" "u_csamul_pg_rca8" +test_circuit "multiplier_unsigned" "u_csamul_cska8" test_circuit "multiplier_unsigned" "u_wallace_cla8" test_circuit "multiplier_unsigned" "u_wallace_rca8" test_circuit "multiplier_unsigned" "u_wallace_pg_rca8" -test_circuit "multiplier_unsigned" "u_wallace_cska8" +test_circuit "multiplier_unsigned" "u_wallace_cska8" +test_circuit "multiplier_unsigned" "u_CSAwallace_cla8" +test_circuit "multiplier_unsigned" "u_CSAwallace_rca8" +test_circuit "multiplier_unsigned" "u_CSAwallace_pg_rca8" +test_circuit "multiplier_unsigned" "u_CSAwallace_cska8" test_circuit "multiplier_unsigned" "u_dadda_cla8" test_circuit "multiplier_unsigned" "u_dadda_rca8" test_circuit "multiplier_unsigned" "u_dadda_pg_rca8" diff --git a/yosys_equiv_check.sh b/yosys_equiv_check.sh index 804f7db..c3098fa 100755 --- a/yosys_equiv_check.sh +++ b/yosys_equiv_check.sh @@ -1,8 +1,8 @@ #!/bin/bash # Script enables formal verification and equivalence of Verilog/BLIF circuit designs -# using Yosys Open SYnthesis Suite by Clifford Wolf. -# For more information, please visit: http://www.clifford.at/yosys/documentation.html +# using Yosys Open SYnthesis Suite by Claire Xenia Wolf. +# For more information, please visit: http://bygone.clairexen.net/yosys/documentation.html # Echo script help help () { @@ -23,6 +23,8 @@ help () { echo " specifies input Verilog design file" echo "-b 'blif_file', --blif_file 'blif_file'" echo " specifies input BLIF design file" + echo "-m 'method', --mode 'method'" + echo " specifies chosen formal equivalence method (sat|equiv)" echo "-H, --hier" echo " specifies whether designs are in hierarchical representation (default is flat)" } @@ -56,6 +58,18 @@ while [[ "$#" -gt 0 ]] ; do exit 1 fi shift 2;; + + "-m" | "--mode") + if [[ "$2" == "sat" || "$2" == "equiv" ]]; then + METHOD="$2" + else + echo "$2 is not a supported formal equivalence method!"; + echo + echo "Type -h | --help for more information." + exit 1 + fi + shift 2;; + "-H" | "--hier") HIERARCHICAL=true shift 1;; @@ -72,9 +86,10 @@ done # Check if both files compulsory parameters are set and if they have the same name. # To proper equiv check both designs top modules must be of same names (assumption that filename == top module name) -if [[ -z "$VERILOG_FILE" || -z "$BLIF_FILE" ]]; then +if [[ -z "$VERILOG_FILE" || -z "$BLIF_FILE" || -z "$METHOD" ]]; then [ -z "$VERILOG_FILE" ] && echo "Missing compulsory Verilog file for comparison!" [ -z "$BLIF_FILE" ] && echo "Missing compulsory BLIF file for comparison!" + [ -z "$METHOD" ] && echo "Missing choice of formal equivalence method!" echo echo "Type -h | --help for more information." exit 1 @@ -92,50 +107,102 @@ else fi # Formal verification with equiv_* for flat designs -if [ "$HIERARCHICAL" = false ]; then - yosys -p " - # Gold design - read_verilog $VERILOG_FILE - prep -top $TOP_MODULE - splitnets -ports;; - design -stash gold +if [ "$METHOD" = "equiv" ]; then + if [ "$HIERARCHICAL" = false ]; then + yosys -p " + # Gold design + read_verilog $VERILOG_FILE + prep -top $TOP_MODULE + splitnets -ports;; + design -stash gold - # Gate design - read_blif $BLIF_FILE - prep -top $TOP_MODULE - design -stash gate + # Gate design + read_blif $BLIF_FILE + prep -top $TOP_MODULE + design -stash gate - # Prove equivalence - design -copy-from gold -as gold $TOP_MODULE - design -copy-from gate -as gate $TOP_MODULE - equiv_make gold gate equiv - hierarchy -top equiv - equiv_simple - equiv_status -assert - " -# Formal verification with equiv_* for hierarchical designs + # Prove equivalence + design -copy-from gold -as gold $TOP_MODULE + design -copy-from gate -as gate $TOP_MODULE + + equiv_make gold gate equiv + hierarchy -top equiv + equiv_simple + equiv_status -assert + " + # Formal verification with equiv_* for hierarchical designs + else + yosys -p " + # Gold design + read_verilog $VERILOG_FILE + prep -top $TOP_MODULE + flatten + splitnets -ports;; + design -stash gold + + # Gate design + read_blif $BLIF_FILE + prep -top $TOP_MODULE + flatten + splitnets -ports;; + design -stash gate + + # Prove equivalence + design -copy-from gold -as gold $TOP_MODULE + design -copy-from gate -as gate $TOP_MODULE + + equiv_make gold gate equiv + hierarchy -top equiv + equiv_simple + equiv_status -assert + " + fi else - yosys -p " - # Gold design - read_verilog $VERILOG_FILE - prep -top $TOP_MODULE - flatten - splitnets -ports;; - design -stash gold + if [ "$HIERARCHICAL" = false ]; then + yosys -p " + # Gold design + read_verilog $VERILOG_FILE + prep -top $TOP_MODULE + splitnets -ports;; + design -stash gold - # Gate design - read_blif $BLIF_FILE - prep -top $TOP_MODULE - flatten - splitnets -ports;; - design -stash gate + # Gate design + read_blif $BLIF_FILE + prep -top $TOP_MODULE + design -stash gate - # Prove equivalence - design -copy-from gold -as gold $TOP_MODULE - design -copy-from gate -as gate $TOP_MODULE - equiv_make gold gate equiv - hierarchy -top equiv - equiv_simple - equiv_status -assert - " + # Prove equivalence + design -copy-from gold -as gold $TOP_MODULE + design -copy-from gate -as gate $TOP_MODULE + + miter -equiv -flatten gold gate miter + hierarchy -top miter + sat -verify -tempinduct -prove trigger 0 + " + # Formal verification with equiv_* for hierarchical designs + else + yosys -p " + # Gold design + read_verilog $VERILOG_FILE + prep -top $TOP_MODULE + flatten + splitnets -ports;; + design -stash gold + + # Gate design + read_blif $BLIF_FILE + prep -top $TOP_MODULE + flatten + splitnets -ports;; + design -stash gate + + # Prove equivalence + design -copy-from gold -as gold $TOP_MODULE + design -copy-from gate -as gate $TOP_MODULE + + miter -equiv -flatten gold gate miter + hierarchy -top miter + sat -verify -tempinduct -prove trigger 0 + " + fi fi