From 5d2f4e07e75a03bf2ce68cede8da42425f668245 Mon Sep 17 00:00:00 2001
From: Honza <jan.klhufek@gmail.com>
Date: Sun, 17 Apr 2022 13:06:46 +0200
Subject: [PATCH] Updated automated testing scripts.
---
.testall.sh | 2 +
README.md | 14 +--
generate_axmuls.py | 69 +++++++++++----
generate_test.py | 90 +++++++++++++++++--
tests/test_all.py | 32 ++++---
tests/test_cgp.py | 14 +--
tests/test_circuits.sh | 38 +++++++-
tests/test_circuits_cgp.sh | 38 +++++++-
tests/test_circuits_verilog.sh | 22 ++++-
yosys_equiv_check.sh | 155 +++++++++++++++++++++++----------
10 files changed, 371 insertions(+), 103 deletions(-)
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