mirror of
https://github.com/ehw-fit/ariths-gen.git
synced 2025-04-03 13:51:33 +01:00
Updated automated testing scripts.
This commit is contained in:
Honza
parent
c0dcf42499
commit
5d2f4e07e7
@ -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
|
||||
14
README.md
14
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.
|
||||
|
||||
@ -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"))
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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 """
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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"
|
||||
|
||||
@ -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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user