3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-05-21 17:39:41 +00:00

Merge branch 'main' into gus/sim-with-vcd-tuneup

This commit is contained in:
nella 2026-05-19 12:17:29 +02:00 committed by GitHub
commit 886d0a7043
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
567 changed files with 17799 additions and 5401 deletions

2
tests/.gitignore vendored
View file

@ -2,3 +2,5 @@
*.out
*.err
run-test.mk
**/Makefile
*.result

127
tests/Makefile Normal file
View file

@ -0,0 +1,127 @@
ifneq ($(wildcard ../Makefile.conf),)
include ../Makefile.conf
endif
OVERRIDE_MAIN=1
include ./common.mk
# Directories with tests not run:
# errors
# lut
# pyosys
# smv
# sva
# tools
# unit
# vloghtb
# Tests that generate Makefile with gen_tests_makefile.py
MK_TEST_DIRS =
MK_TEST_DIRS += ./arch/analogdevices
MK_TEST_DIRS += ./arch/anlogic
MK_TEST_DIRS += ./arch/ecp5
MK_TEST_DIRS += ./arch/efinix
MK_TEST_DIRS += ./arch/fabulous
MK_TEST_DIRS += ./arch/gatemate
MK_TEST_DIRS += ./arch/gowin
MK_TEST_DIRS += ./arch/ice40
MK_TEST_DIRS += ./arch/intel_alm
MK_TEST_DIRS += ./arch/machxo2
MK_TEST_DIRS += ./arch/microchip
MK_TEST_DIRS += ./arch/nanoxplore
MK_TEST_DIRS += ./arch/nexus
MK_TEST_DIRS += ./arch/quicklogic/pp3
MK_TEST_DIRS += ./arch/quicklogic/qlf_k6n10f
MK_TEST_DIRS += ./arch/xilinx
MK_TEST_DIRS += ./bind
MK_TEST_DIRS += ./bugpoint
MK_TEST_DIRS += ./opt
MK_TEST_DIRS += ./sat
MK_TEST_DIRS += ./sdc
MK_TEST_DIRS += ./sim
MK_TEST_DIRS += ./svtypes
MK_TEST_DIRS += ./techmap
MK_TEST_DIRS += ./various
MK_TEST_DIRS += ./rtlil
ifeq ($(ENABLE_VERIFIC),1)
ifneq ($(YOSYS_NOVERIFIC),1)
MK_TEST_DIRS += ./verific
endif
endif
MK_TEST_DIRS += ./verilog
MK_TEST_DIRS += ./arith_tree
MK_TEST_DIRS += ./simple
MK_TEST_DIRS += ./simple_abc9
MK_TEST_DIRS += ./hana
MK_TEST_DIRS += ./asicworld
MK_TEST_DIRS += ./realmath
MK_TEST_DIRS += ./share
MK_TEST_DIRS += ./opt_share
MK_TEST_DIRS += ./fsm
MK_TEST_DIRS += ./memlib
MK_TEST_DIRS += ./bram
MK_TEST_DIRS += ./svinterfaces
MK_TEST_DIRS += ./xprop
MK_TEST_DIRS += ./select
MK_TEST_DIRS += ./peepopt
MK_TEST_DIRS += ./proc
MK_TEST_DIRS += ./blif
MK_TEST_DIRS += ./arch
MK_TEST_DIRS += ./rpc
MK_TEST_DIRS += ./memfile
MK_TEST_DIRS += ./fmt
MK_TEST_DIRS += ./cxxrtl
MK_TEST_DIRS += ./liberty
#ifeq ($(ENABLE_FUNCTIONAL_TESTS),1)
#MK_TEST_DIRS += ./functional
#endif
MK_TEST_DIRS += ./memories
MK_TEST_DIRS += ./aiger
MK_TEST_DIRS += ./alumacc
all: vanilla-test
# makefile-./ is a dummy string, not a directory
.PHONY: makefile-tests
.SILENT: $(MK_TEST_DIRS:%=%/Makefile)
makefile-tests: $(MK_TEST_DIRS:%=makefile-./%)
prep: $(MK_TEST_DIRS:%=%/Makefile)
@echo "All Makefiles generated."
.PHONY: force-create
# this target actually emits Makefile files
%/Makefile: force-create
+@cd $* && python3 generate_mk.py
makefile-./%: %/Makefile
@$(MAKE) -C $*
@echo "...passed tests in $*"
.PHONY: functional
functional:
ifeq ($(ENABLE_FUNCTIONAL_TESTS),1)
@cd functional && ./run-test.sh
endif
vanilla-test: prep makefile-tests functional
@echo ""
@echo " Passed \"make vanilla-test\"."
ifeq ($(ENABLE_VERIFIC),1)
ifeq ($(YOSYS_NOVERIFIC),1)
@echo " Ran tests without verific support due to YOSYS_NOVERIFIC=1."
endif
endif
@echo ""
@$(MAKE) --no-print-directory summary
clean:
@rm -rf ./asicworld/*.out ./asicworld/*.log
@rm -rf ./hana/*.out ./hana/*.log
@rm -rf ./simple/*.out ./simple/*.log
@rm -rf ./memories/*.out ./memories/*.log ./memories/*.dmp
@rm -rf ./sat/*.log ./techmap/*.log ./various/*.log
@rm -rf ./bram/temp ./fsm/temp ./realmath/temp ./share/temp ./smv/temp ./various/temp
@rm -f ./svinterfaces/*.log_stdout ./svinterfaces/*.log_stderr ./svinterfaces/dut_result.txt ./svinterfaces/reference_result.txt ./svinterfaces/a.out ./svinterfaces/*_syn.v ./svinterfaces/*.diff
@rm -f ./tools/cmp_tbdata
@rm -f $(addsuffix /Makefile,$(MK_TEST_DIRS))
@find . -name '*.result' -type f -exec rm -f {} +

View file

@ -0,0 +1,66 @@
#!/usr/bin/env python3
import sys
sys.path.append("..")
import gen_tests_makefile
import glob
import os
def base(fn):
return os.path.splitext(fn)[0]
def cmd(lines):
return " \\\n".join(lines)
# NB: *.aag and *.aig must contain a symbol table naming the primary
# inputs and outputs, otherwise ABC and Yosys will name them
# arbitrarily (and inconsistently with each other).
# Since ABC cannot read *.aag, read the *.aig instead
# (which would have been created by the reference aig2aig utility,
# available from http://fmv.jku.at/aiger/)
def create_tests():
aags = sorted(glob.glob("*.aag"))
yss = sorted(glob.glob("*.ys"))
for aag in aags:
b = base(aag)
gen_tests_makefile.generate_target(aag, cmd([
f"$(ABC) -q \"read -c {b}.aig; write {b}_ref.v\";",
"$(YOSYS) -qp \"",
f"read_verilog {b}_ref.v;",
"prep;",
"design -stash gold;",
f"read_aiger -clk_name clock {aag};",
"prep;",
"design -stash gate;",
"design -import gold -as gold;",
"design -import gate -as gate;",
"miter -equiv -flatten -make_assert -make_outputs gold gate miter;",
"sat -verify -prove-asserts -show-ports -seq 16 miter;",
f"\" -l {aag}.log"
]))
# ---- Yosys script tests ----
for ys in yss:
gen_tests_makefile.generate_ys_test(ys)
gen_tests_makefile.generate_target("aigmap", cmd([
"rm -rf gate; mkdir gate;",
"$(YOSYS) --no-version -p \"test_cell -aigmap -w gate/ -n 1 -s 1 all\";",
"set -o pipefail; diff --brief gold gate | tee aigmap.err;",
"rm -f aigmap.err"
]))
extra = [
"ifneq ($(ABCEXTERNAL),)",
"ABC ?= $(ABCEXTERNAL)",
"else",
f"ABC ?= {gen_tests_makefile.yosys_basedir}/yosys-abc",
"endif",
"SHELL := /usr/bin/env bash",
]
gen_tests_makefile.generate_custom(create_tests, extra)

View file

@ -1,70 +0,0 @@
#!/usr/bin/env bash
source ../common-env.sh
set -e
OPTIND=1
abcprog="../../yosys-abc" # default to built-in version of abc
while getopts "A:" opt
do
case "$opt" in
A) abcprog="$OPTARG" ;;
esac
done
shift "$((OPTIND-1))"
# NB: *.aag and *.aig must contain a symbol table naming the primary
# inputs and outputs, otherwise ABC and Yosys will name them
# arbitrarily (and inconsistently with each other).
for aag in *.aag; do
# Since ABC cannot read *.aag, read the *.aig instead
# (which would have been created by the reference aig2aig utility,
# available from http://fmv.jku.at/aiger/)
echo "Checking $aag."
$abcprog -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
../../yosys -qp "
read_verilog ${aag%.*}_ref.v
prep
design -stash gold
read_aiger -clk_name clock $aag
prep
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports -seq 16 miter
" -l ${aag}.log
done
for aig in *.aig; do
echo "Checking $aig."
$abcprog -q "read -c $aig; write ${aig%.*}_ref.v"
../../yosys -qp "
read_verilog ${aig%.*}_ref.v
prep
design -stash gold
read_aiger -clk_name clock $aig
prep
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports -seq 16 miter
" -l ${aig}.log
done
for y in *.ys; do
echo "Running $y."
../../yosys -ql ${y%.*}.log $y
done
# compare aigmap with reference
# make gold with: rm gold/*; yosys --no-version -p "test_cell -aigmap -w gold/ -n 1 -s 1 all"
rm -rf gate; mkdir gate
../../yosys --no-version -p "test_cell -aigmap -w gate/ -n 1 -s 1 all"
(
set -o pipefail
diff --brief gold gate | tee aigmap.err
)
rm aigmap.err

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts"])

View file

@ -1,7 +0,0 @@
#!/usr/bin/env bash
source ../common-env.sh
set -e
for x in *.ys; do
echo "Running $x.."
../../yosys -ql ${x%.ys}.log $x
done

1
tests/arch/analogdevices/.gitignore vendored Normal file
View file

@ -0,0 +1 @@
t_*.ys

View file

@ -0,0 +1,13 @@
read_verilog ../common/add_sub.v
hierarchy -top top
proc
design -save orig
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 8 t:LUT2
select -assert-count 2 t:CRY4
select -assert-count 2 t:CRY4INIT
select -assert-none t:LUT2 t:CRY4 t:CRY4INIT %% t:* %D

View file

@ -0,0 +1,47 @@
read_verilog ../common/adffs.v
design -save read
hierarchy -top adff
proc
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd adff # Constrain all select calls below inside the top module
select -assert-count 1 t:FFCE
select -assert-none t:FFCE %% t:* %D
design -load read
hierarchy -top adffn
proc
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd adffn # Constrain all select calls below inside the top module
select -assert-count 1 t:FFCE
select -assert-count 1 t:LUT1
select -assert-none t:FFCE t:LUT1 %% t:* %D
design -load read
hierarchy -top dffs
proc
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:FFRE
select -assert-count 1 t:LUT2
stat
select -assert-none t:FFRE t:LUT2 %% t:* %D
design -load read
hierarchy -top ndffnr
proc
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:FFRE_N
select -assert-count 1 t:LUT1
select -assert-none t:FFRE_N t:LUT1 %% t:* %D

View file

@ -0,0 +1,50 @@
# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RBRAM2
# w4b | r16b
design -reset
read_verilog asym_ram_sdp_read_wider.v
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
select -assert-count 1 t:RBRAM2
# w8b | r16b
design -reset
read_verilog asym_ram_sdp_read_wider.v
chparam -set WIDTHA 8 -set SIZEA 512 -set ADDRWIDTHA 9 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
select -assert-count 1 t:RBRAM2
# w4b | r32b
design -reset
read_verilog asym_ram_sdp_read_wider.v
chparam -set WIDTHB 32 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
select -assert-count 2 t:RBRAM2
# w16b | r4b
design -reset
read_verilog asym_ram_sdp_write_wider.v
synth_analogdevices -top asym_ram_sdp_write_wider -noiopad
select -assert-count 1 t:RBRAM2
# w16b | r8b
design -reset
read_verilog asym_ram_sdp_write_wider.v
chparam -set WIDTHB 8 -set SIZEB 512 -set ADDRWIDTHB 9 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_write_wider -noiopad
select -assert-count 1 t:RBRAM2
# w32b | r4b
design -reset
read_verilog asym_ram_sdp_write_wider.v
chparam -set WIDTHA 32 -set SIZEA 128 -set ADDRWIDTHA 7 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_write_wider -noiopad
select -assert-count 1 t:RBRAM2
# w4b | r24b
design -reset
read_verilog asym_ram_sdp_read_wider.v
chparam -set SIZEA 768
chparam -set WIDTHB 24 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
select -assert-count 2 t:RBRAM2

View file

@ -0,0 +1,73 @@
// Asymmetric port RAM
// Read Wider than Write. Read Statement in loop
//asym_ram_sdp_read_wider.v
module asym_ram_sdp_read_wider (clkA, clkB, enaA, weA, enaB, addrA, addrB, diA, doB);
parameter WIDTHA = 4;
parameter SIZEA = 1024;
parameter ADDRWIDTHA = 10;
parameter WIDTHB = 16;
parameter SIZEB = 256;
parameter ADDRWIDTHB = 8;
input clkA;
input clkB;
input weA;
input enaA, enaB;
input [ADDRWIDTHA-1:0] addrA;
input [ADDRWIDTHB-1:0] addrB;
input [WIDTHA-1:0] diA;
output [WIDTHB-1:0] doB;
`define max(a,b) {(a) > (b) ? (a) : (b)}
`define min(a,b) {(a) < (b) ? (a) : (b)}
function integer log2;
input integer value;
reg [31:0] shifted;
integer res;
begin
if (value < 2)
log2 = value;
else
begin
shifted = value-1;
for (res=0; shifted>0; res=res+1)
shifted = shifted>>1;
log2 = res;
end
end
endfunction
localparam maxSIZE = `max(SIZEA, SIZEB);
localparam maxWIDTH = `max(WIDTHA, WIDTHB);
localparam minWIDTH = `min(WIDTHA, WIDTHB);
localparam RATIO = maxWIDTH / minWIDTH;
localparam log2RATIO = log2(RATIO);
(* ram_style="block" *)
reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
reg [WIDTHB-1:0] readB;
always @(posedge clkA)
begin
if (enaA) begin
if (weA)
RAM[addrA] <= diA;
end
end
always @(posedge clkB)
begin : ramread
integer i;
reg [log2RATIO-1:0] lsbaddr;
if (enaB) begin
for (i = 0; i < RATIO; i = i+1) begin
lsbaddr = i;
readB[(i+1)*minWIDTH-1 -: minWIDTH] <= RAM[{addrB, lsbaddr}];
end
end
end
assign doB = readB;
endmodule

View file

@ -0,0 +1,72 @@
// Asymmetric port RAM
// Write wider than Read. Write Statement in a loop.
// asym_ram_sdp_write_wider.v
module asym_ram_sdp_write_wider (clkA, clkB, weA, enaA, enaB, addrA, addrB, diA, doB);
parameter WIDTHB = 4;
parameter SIZEB = 1024;
parameter ADDRWIDTHB = 10;
parameter WIDTHA = 16;
parameter SIZEA = 256;
parameter ADDRWIDTHA = 8;
input clkA;
input clkB;
input weA;
input enaA, enaB;
input [ADDRWIDTHA-1:0] addrA;
input [ADDRWIDTHB-1:0] addrB;
input [WIDTHA-1:0] diA;
output [WIDTHB-1:0] doB;
`define max(a,b) {(a) > (b) ? (a) : (b)}
`define min(a,b) {(a) < (b) ? (a) : (b)}
function integer log2;
input integer value;
reg [31:0] shifted;
integer res;
begin
if (value < 2)
log2 = value;
else
begin
shifted = value-1;
for (res=0; shifted>0; res=res+1)
shifted = shifted>>1;
log2 = res;
end
end
endfunction
localparam maxSIZE = `max(SIZEA, SIZEB);
localparam maxWIDTH = `max(WIDTHA, WIDTHB);
localparam minWIDTH = `min(WIDTHA, WIDTHB);
localparam RATIO = maxWIDTH / minWIDTH;
localparam log2RATIO = log2(RATIO);
(* ram_style="block" *)
reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
reg [WIDTHB-1:0] readB;
always @(posedge clkB) begin
if (enaB) begin
readB <= RAM[addrB];
end
end
assign doB = readB;
always @(posedge clkA)
begin : ramwrite
integer i;
reg [log2RATIO-1:0] lsbaddr;
for (i=0; i< RATIO; i= i+ 1) begin : write1
lsbaddr = i;
if (enaA) begin
if (weA)
RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH];
end
end
end
endmodule

View file

@ -0,0 +1,39 @@
# Check that blockram memory without parameters is not modified
read_verilog ../common/memory_attributes/attributes_test.v
hierarchy -top block_ram
synth_analogdevices -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module
# select -assert-count 1 t:RBRAM2 # This currently infers LUTRAM because BRAM is expensive.
# Check that distributed memory without parameters is not modified
design -reset
read_verilog ../common/memory_attributes/attributes_test.v
hierarchy -top distributed_ram
synth_analogdevices -top distributed_ram -noiopad
cd distributed_ram # Constrain all select calls below inside the top module
select -assert-count 8 t:RAMS64X1
select -assert-count 8 t:FFRE
# Set ram_style distributed to blockram memory; will be implemented as distributed
design -reset
read_verilog ../common/memory_attributes/attributes_test.v
setattr -set ram_style "distributed" block_ram/m:*
synth_analogdevices -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module
select -assert-count 64 t:RAMS64X1
select -assert-count 4 t:FFRE
# Set synthesis, logic_block to blockram memory; will be implemented as distributed
design -reset
read_verilog ../common/memory_attributes/attributes_test.v
setattr -set logic_block 1 block_ram/m:*
synth_analogdevices -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module
select -assert-count 0 t:RBRAM2
# Set ram_style block to a distributed memory; will be implemented as blockram
design -reset
read_verilog ../common/memory_attributes/attributes_test.v
synth_analogdevices -top distributed_ram_manual -noiopad
cd distributed_ram_manual # Constrain all select calls below inside the top module
# select -assert-count 1 t:RBRAM2 # This gets implemented in logic instead

View file

@ -0,0 +1,77 @@
### TODO: Not running equivalence checking because BRAM models does not exists
### currently. Checking instance counts instead.
# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RBRAM2
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 12 -set DATA_WIDTH 1 sync_ram_sdp
setattr -set ram_style "block" sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RBRAM2
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp
setattr -set ram_style "block" sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RBRAM2
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp
setattr -set ram_style "block" sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RBRAM2
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RBRAM2
# Anything memory bits < 1024 -> LUTRAM
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 0 t:RBRAM2
select -assert-count 8 t:RAMD64X1
select -assert-count 2 t:FFRE
# More than 18K bits, data width <= 36 (TDP), and address width from 10 to 15b (non-cascaded) -> RAMB36E1
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RBRAM2
### With parameters
design -reset
read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 12 -chparam DATA_WIDTH 1
setattr -set ram_style "block" m:memory
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RBRAM2
design -reset
read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 12 -chparam DATA_WIDTH 1
setattr -set logic_block 1 m:memory
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 0 t:RBRAM2
design -reset
read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
setattr -set ram_style "block" m:memory
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RBRAM2

View file

@ -0,0 +1,34 @@
read_verilog <<EOT
module register_file(
input wire clk,
input wire write_enable,
input wire [63:0] write_data,
input wire [4:0] write_reg,
input wire [4:0] read1_reg,
input wire [4:0] read2_reg,
input wire [4:0] read3_reg,
output reg [63:0] read1_data,
output reg [63:0] read2_data,
output reg [63:0] read3_data
);
reg [63:0] registers[0:31];
always @(posedge clk) begin
if (write_enable == 1'b1) begin
registers[write_reg] <= write_data;
end
end
always @(all) begin
read1_data <= registers[read1_reg];
read2_data <= registers[read2_reg];
read3_data <= registers[read3_reg];
end
endmodule
EOT
synth_analogdevices -noiopad
cd register_file
select -assert-count 192 t:RAMD32X1
select -assert-none t:RAMD32X1 %% t:* %D

View file

@ -0,0 +1,11 @@
read_verilog << EOF
module top(...);
input wire [31:0] A;
output wire [31:0] P;
assign P = A * 32'h12300000;
endmodule
EOF
synth_analogdevices

View file

@ -0,0 +1,18 @@
read_verilog << EOF
module top(...);
input signed [17:0] A;
input signed [17:0] B;
output X;
output Y;
wire [35:0] P;
assign P = A * B;
assign X = P[0];
assign Y = P[35];
endmodule
EOF
synth_analogdevices

View file

@ -0,0 +1,16 @@
read_verilog <<EOT
module led_blink (
input clk,
output ledc
);
reg [6:0] led_counter = 0;
always @( posedge clk ) begin
led_counter <= led_counter + 1;
end
assign ledc = !led_counter[ 6:3 ];
endmodule
EOT
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices

View file

@ -0,0 +1,13 @@
read_verilog ../common/counter.v
hierarchy -top top
proc
flatten
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 8 t:FFCE
select -assert-count 1 t:LUT1
select -assert-count 2 t:CRY4
select -assert-count 1 t:CRY4INIT
select -assert-none t:FFCE t:LUT1 t:CRY4 t:CRY4INIT %% t:* %D

View file

@ -0,0 +1,41 @@
read_verilog ../common/dffs.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
select -assert-count 1 t:FFRE
select -assert-none t:FFRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:FFRE
select -assert-none t:FFRE %% t:* %D
design -load read
hierarchy -top dff
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
select -assert-count 1 t:FFRE
select -assert-none t:FFRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:FFRE
select -assert-none t:FFRE %% t:* %D

View file

@ -0,0 +1,42 @@
logger -nowarn "Yosys has only limited support for tri-state logic at the moment\. .*"
logger -nowarn "Ignoring boxed module .*\."
read_verilog <<EOT
module top(input [24:0] A, input [17:0] B, output [47:0] P);
DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P));
endmodule
EOT
techmap -autoproc -wb -map +/analogdevices/cells_sim.v
opt
scc -expect 0
design -reset
read_verilog <<EOT
module top(input signed [24:0] A, input signed [17:0] B, output [47:0] P);
assign P = A * B;
endmodule
EOT
synth_analogdevices
techmap -autoproc -wb -map +/analogdevices/cells_sim.v
opt -full -fine
select -assert-count 2 t:$mul
select -assert-count 0 t:* t:$mul %D
design -reset
read_verilog -icells -formal <<EOT
module top(output [43:0] P);
\$__MUL22X22 mul (.A(42), .B(42), .Y(P));
assert property (P == 42*42);
endmodule
EOT
async2sync
techmap -map +/analogdevices/dsp_map.v
verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
synth_analogdevices
techmap -autoproc -wb -map +/analogdevices/cells_sim.v
opt -full -fine
select -assert-count 0 t:* t:$assert %d
sat -verify -prove-asserts

View file

@ -0,0 +1,20 @@
read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
design -save orig
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
miter -equiv -make_assert -flatten gold gate miter
sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
stat
select -assert-count 6 t:FFRE
select -assert-count 1 t:LUT1
select -assert-count 1 t:LUT3
select -assert-count 1 t:LUT4
select -assert-count 5 t:LUT5
select -assert-none t:FFRE t:LUT1 t:LUT3 t:LUT4 t:LUT5 %% t:* %D

View file

@ -0,0 +1,9 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
import mem_gen
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -0,0 +1,11 @@
read_verilog ../common/logic.v
hierarchy -top top
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT1
select -assert-count 6 t:LUT2
select -assert-count 2 t:LUT4
select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D

View file

@ -0,0 +1,113 @@
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 5
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w1r
select -assert-count 8 t:FFRE
select -assert-count 8 t:RAMS64X1
select -assert-none t:FFRE t:RAMS64X1 %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w1r
dump
select -assert-count 8 t:FFRE
select -assert-count 8 t:RAMS64X1
select -assert-none t:FFRE t:RAMS64X1 %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w3r
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w3r
select -assert-count 24 t:FFRE
select -assert-count 16 t:RAMD32X1
select -assert-none t:FFRE t:RAMD32X1 %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w3r -chparam A_WIDTH 6
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w3r
select -assert-count 24 t:FFRE
select -assert-count 16 t:RAMD64X1
select -assert-none t:FFRE t:RAMD64X1 %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w1r
select -assert-count 6 t:FFRE
select -assert-count 6 t:RAMS64X1
select -assert-none t:FFRE t:RAMS64X1 %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w1r
select -assert-count 6 t:FFRE
select -assert-count 6 t:RAMS64X1
select -assert-none t:FFRE t:RAMS64X1 %% t:* %D

View file

@ -0,0 +1,121 @@
from __future__ import annotations
from dataclasses import dataclass
blockram_template = """# ======================================
log ** GENERATING TEST {top} WITH PARAMS{param_str}
design -reset; read_verilog -defer ../common/blockram.v
chparam{param_str} {top}
hierarchy -top {top}
echo on
debug synth_analogdevices -tech {tech} -top {top} {opts} -run :map_ffram
stat; echo off
"""
inference_tests: "list[tuple[str, list[tuple[str, int]], str, list[str], list[str]]]" = [
# RBRAM2 has TDP and SDP for 8192x5bit, 4096x9bit, and 2048x40bit
("t16ffc", [("ADDRESS_WIDTH", 13), ("DATA_WIDTH", 5)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
("t16ffc", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 9)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
("t16ffc", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 40)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
# LUTRAM is generally cheaper than BRAM for undersized (SDP) memories
("t16ffc", [("ADDRESS_WIDTH", 6), ("DATA_WIDTH", 1)], "sync_ram_sdp", ["-assert-count 1 t:RAMD64X1"], []),
("t16ffc", [("ADDRESS_WIDTH", 6), ("DATA_WIDTH", 8)], "sync_ram_sdp", ["-assert-count 8 t:RAMD64X1"], []),
("t16ffc", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 8)], "sync_ram_sdp", ["-assert-count 128 t:RAMD64X1"], []),
("t16ffc", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 16)], "sync_ram_sdp", ["-assert-count 256 t:RAMD64X1"], []),
# RBRAM is half the depth of RBRAM2, and doesn't have TDP, also LUTRAM is cheaper, so we need to specify not to use it
("t40lp", [("ADDRESS_WIDTH", 13), ("DATA_WIDTH", 5)], "sync_ram_sdp", ["-assert-count 2 t:RBRAM"], ["-nolutram"]),
("t40lp", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 5)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
("t40lp", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 9)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
("t40lp", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 40)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
# 2048x32 and 2048x36bit are also valid
("t16ffc", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 32)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
("t16ffc", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 36)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
("t40lp", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 32)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
("t40lp", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 36)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
# 4096x16/18bit can be mapped to a single 2048x32/36bit
("t16ffc", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 16)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
("t16ffc", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 18)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
("t40lp", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 16)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
("t40lp", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 18)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
# same for 8192x8/9bit
("t16ffc", [("ADDRESS_WIDTH", 13), ("DATA_WIDTH", 8)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
("t16ffc", [("ADDRESS_WIDTH", 13), ("DATA_WIDTH", 9)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
("t40lp", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 8)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
("t40lp", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 9)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
# but 4096x20bit requires extra memories because 2048x40bit has 8bit byte enables (which doesn't divide 20bit evenly)
("t16ffc", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 20)], "sync_ram_sdp", ["-assert-count 2 t:RBRAM2"], []),
("t40lp", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 20)], "sync_ram_sdp", ["-assert-count 2 t:RBRAM"], ["-nolutram"]),
]
@dataclass
class TestClass:
params: dict[str, int]
top: str
assertions: list[str]
test_steps: None | list[dict[str, int]]
opts: list[str]
tech: str = "t16ffc"
sim_tests: list[TestClass] = []
for (tech, params, top, assertions, opts) in inference_tests:
sim_test = TestClass(
params=dict(params),
top=top,
assertions=assertions,
test_steps=None,
opts=opts,
tech=tech,
)
sim_tests.append(sim_test)
i = 0
j = 0
max_j = 16
f = None
for sim_test in sim_tests:
# format params
param_str = ""
for (key, val) in sim_test.params.items():
param_str += f" -set {key} {val}"
# resolve top module wildcards
top_list = [sim_test.top]
if "*dp" in sim_test.top:
top_list += [
sim_test.top.replace("*dp", dp_sub) for dp_sub in ["sdp", "tdp"]
]
if "w*r" in sim_test.top:
top_list += [
sim_test.top.replace("w*r", wr_sub) for wr_sub in ["wwr", "wrr"]
]
if len(top_list) > 1:
top_list.pop(0)
# iterate over string substitutions
for top in top_list:
# limit number of tests per file to allow parallel make
if not f:
fn = f"t_mem{i}.ys"
f = open(fn, mode="w")
j = 0
# output yosys script test file
print(
blockram_template.format(param_str=param_str, top=top, tech=sim_test.tech, opts=" ".join(sim_test.opts)),
file=f
)
for assertion in sim_test.assertions:
print(f"log ** CHECKING CELL COUNTS FOR TEST {top} WITH PARAMS{param_str} ON TECH {sim_test.tech}", file=f)
print(f"select {assertion}", file=f)
print("", file=f)
# increment test counter
j += 1
if j >= max_j:
f = f.close()
i += 1
if f:
f.close()

View file

@ -0,0 +1,9 @@
read_verilog ../common/mul.v
hierarchy -top top
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:RBBDSP
select -assert-none t:RBBDSP %% t:* %D

View file

@ -0,0 +1,30 @@
/*
Example from: https://www.xilinx.com/support/documentation/sw_manuals/xilinx2019_1/ug901-vivado-synthesis.pdf [p. 89].
*/
// Unsigned 16x24-bit Multiplier
// 1 latency stage on operands
// 3 latency stage after the multiplication
// File: multipliers2.v
//
module mul_unsigned (clk, A, B, RES);
parameter WIDTHA = /*16*/ 6;
parameter WIDTHB = /*24*/ 9;
input clk;
input [WIDTHA-1:0] A;
input [WIDTHB-1:0] B;
output [WIDTHA+WIDTHB-1:0] RES;
reg [WIDTHA-1:0] rA;
reg [WIDTHB-1:0] rB;
reg [WIDTHA+WIDTHB-1:0] M [3:0];
integer i;
always @(posedge clk)
begin
rA <= A;
rB <= B;
M[0] <= rA * rB;
for (i = 0; i < 3; i = i+1)
M[i+1] <= M[i];
end
assign RES = M[3];
endmodule

View file

@ -0,0 +1,10 @@
read_verilog mul_unsigned.v
hierarchy -top mul_unsigned
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mul_unsigned # Constrain all select calls below inside the top module
select -assert-count 1 t:RBBDSP
select -assert-count 75 t:FFRE
select -assert-none t:RBBDSP t:FFRE %% t:* %D

View file

@ -0,0 +1,50 @@
read_verilog ../common/mux.v
design -save read
hierarchy -top mux2
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux2 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3
select -assert-none t:LUT3 %% t:* %D
design -load read
hierarchy -top mux4
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux4 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT6
select -assert-none t:LUT6 %% t:* %D
design -load read
hierarchy -top mux8
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux8 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3
select -assert-count 2 t:LUT6
select -assert-none t:LUT3 t:LUT6 %% t:* %D
design -load read
hierarchy -top mux16
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module
select -assert-max 2 t:LUT3
select -assert-max 2 t:LUT4
select -assert-min 4 t:LUT6
select -assert-max 7 t:LUT6
select -assert-max 2 t:LUTMUX7
dump
select -assert-none t:LUT6 t:LUT4 t:LUT3 t:LUTMUX7 %% t:* %D

View file

@ -0,0 +1,26 @@
read_rtlil << EOF
module \top
wire width 4 input 1 \A
wire output 2 \O
cell \LUT4 $0
parameter \INIT 16'1111110011000000
connect \I0 \A [0]
connect \I1 \A [1]
connect \I2 \A [2]
connect \I3 \A [3]
connect \O \O
end
end
EOF
read_verilog -lib +/analogdevices/cells_sim.v
equiv_opt -assert -map +/analogdevices/cells_sim.v opt_lut_ins -tech analogdevices
design -load postopt
select -assert-count 1 t:LUT3

View file

@ -0,0 +1,10 @@
read_verilog ../common/shifter.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 8 t:FFRE
select -assert-none t:FFRE %% t:* %D

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -22,6 +22,30 @@ module sync_ram_sp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
endmodule // sync_ram_sp
module sync_ram_sp_nochange #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
(input wire write_enable, clk,
input wire [DATA_WIDTH-1:0] data_in,
input wire [ADDRESS_WIDTH-1:0] address_in,
output wire [DATA_WIDTH-1:0] data_out);
localparam WORD = (DATA_WIDTH-1);
localparam DEPTH = (2**ADDRESS_WIDTH-1);
reg [WORD:0] data_out_r;
reg [WORD:0] memory [0:DEPTH];
always @(posedge clk) begin
if (write_enable)
memory[address_in] <= data_in;
else
data_out_r <= memory[address_in];
end
assign data_out = data_out_r;
endmodule // sync_ram_sp_nochange
module sync_ram_sdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
(input wire clk, write_enable,
input wire [DATA_WIDTH-1:0] data_in,
@ -112,6 +136,62 @@ module sync_ram_sdp_wrr #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10, SHIFT_VAL=1)
endmodule // sync_ram_sdp_wrr
module double_sync_ram_sp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10, USE_TDP=0)
(
input wire write_enable_a, clk_a,
input wire [DATA_WIDTH-1:0] data_in_a,
input wire [ADDRESS_WIDTH-1:0] address_in_a,
output wire [DATA_WIDTH-1:0] data_out_a,
input wire write_enable_b, clk_b,
input wire [DATA_WIDTH-1:0] data_in_b,
input wire [ADDRESS_WIDTH-1:0] address_in_b,
output wire [DATA_WIDTH-1:0] data_out_b
);
generate
if (USE_TDP) begin
sync_ram_tdp #(
.DATA_WIDTH(DATA_WIDTH),
.ADDRESS_WIDTH(ADDRESS_WIDTH+1)
) ram (
.clk_a(clk_a), .clk_b(clk_b),
.write_enable_a(write_enable_a), .write_enable_b(write_enable_b),
.write_data_a(data_in_a), .write_data_b(data_in_b),
.addr_a({1'b0, address_in_a}), .addr_b({1'b1, address_in_b}),
.read_data_a(data_out_a), .read_data_b(data_out_b)
);
end else begin
sync_ram_sp #(
.DATA_WIDTH(DATA_WIDTH),
.ADDRESS_WIDTH(ADDRESS_WIDTH)
) a_ram (
.write_enable(write_enable_a),
.clk(clk_a),
.data_in(data_in_a),
.address_in(address_in_a),
.data_out(data_out_a)
);
sync_ram_sp #(
.DATA_WIDTH(DATA_WIDTH),
.ADDRESS_WIDTH(ADDRESS_WIDTH)
) b_ram (
.write_enable(write_enable_b),
.clk(clk_b),
.data_in(data_in_b),
.address_in(address_in_b),
.data_out(data_out_b)
);
end
endgenerate
endmodule // double_sync_ram_sp
module double_sync_ram_sdp #(parameter DATA_WIDTH_A=8, ADDRESS_WIDTH_A=10, DATA_WIDTH_B=8, ADDRESS_WIDTH_B=10)
(
input wire write_enable_a, clk_a,

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -23,7 +23,7 @@ EOF
read_verilog -lib +/ecp5/cells_sim.v
equiv_opt -assert -map +/ecp5/cells_sim.v opt_lut_ins -tech ecp5
equiv_opt -assert -map +/ecp5/cells_sim.v opt_lut_ins -tech lattice
design -load postopt

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -13,7 +13,7 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
cd fsm # Constrain all select calls below inside the top module
select -assert-count 6 t:LUTFF
select -assert-max 4 t:LUT2
select -assert-max 2 t:LUT3
select -assert-max 9 t:LUT4
select -assert-max 5 t:LUT2
select -assert-max 4 t:LUT3
select -assert-max 8 t:LUT4
select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,9 +1,29 @@
read_verilog ../common/add_sub.v
hierarchy -top top
proc
design -save orig
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 8 t:CC_ADDF
select -assert-max 4 t:CC_LUT1
select -assert-none t:CC_ADDF t:CC_LUT1 %% t:* %D
design -load orig
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 8 t:CC_ADDF
select -assert-max 4 t:CC_LUT1
select -assert-none t:CC_ADDF t:CC_LUT1 %% t:* %D
design -load orig
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 8 t:CC_ADDF
select -assert-max 4 t:CC_LUT1
select -assert-none t:CC_ADDF t:CC_LUT1 %% t:* %D

View file

@ -31,6 +31,28 @@ select -assert-count 1 t:CC_DFF
select -assert-max 1 t:CC_LUT2
select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
design -load read
hierarchy -top dffs
proc
equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_BUFG
select -assert-count 1 t:CC_DFF
select -assert-max 1 t:CC_LUT2
select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
design -load read
hierarchy -top dffs
proc
equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_BUFG
select -assert-count 1 t:CC_DFF
select -assert-max 1 t:CC_LUT2
select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
design -load read
hierarchy -top ndffnr
proc
@ -41,3 +63,25 @@ select -assert-count 1 t:CC_BUFG
select -assert-count 1 t:CC_DFF
select -assert-max 1 t:CC_LUT2
select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
design -load read
hierarchy -top ndffnr
proc
equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_BUFG
select -assert-count 1 t:CC_DFF
select -assert-max 1 t:CC_LUT2
select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D
design -load read
hierarchy -top ndffnr
proc
equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_BUFG
select -assert-count 1 t:CC_DFF
select -assert-max 1 t:CC_LUT2
select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D

View file

@ -2,6 +2,9 @@ read_verilog ../common/counter.v
hierarchy -top top
proc
flatten
design -save orig
equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
@ -10,3 +13,25 @@ select -assert-count 8 t:CC_ADDF
select -assert-count 1 t:CC_BUFG
select -assert-count 8 t:CC_DFF
select -assert-none t:CC_ADDF t:CC_BUFG t:CC_DFF %% t:* %D
design -load orig
equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 8 t:CC_ADDF
select -assert-count 1 t:CC_BUFG
select -assert-count 8 t:CC_DFF
select -assert-none t:CC_ADDF t:CC_BUFG t:CC_DFF %% t:* %D
design -load orig
equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 8 t:CC_ADDF
select -assert-count 1 t:CC_BUFG
select -assert-count 8 t:CC_DFF
select -assert-none t:CC_ADDF t:CC_BUFG t:CC_DFF %% t:* %D

View file

@ -3,6 +3,8 @@ hierarchy -top fsm
proc
flatten
design -save orig
equiv_opt -run :prove -map +/gatemate/cells_sim.v synth_gatemate -noiopad
async2sync
miter -equiv -make_assert -flatten gold gate miter
@ -18,3 +20,42 @@ select -assert-max 5 t:CC_LUT2
select -assert-max 6 t:CC_LUT3
select -assert-max 9 t:CC_LUT4
select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 t:CC_LUT3 t:CC_LUT4 %% t:* %D
design -load orig
equiv_opt -run :prove -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree
async2sync
miter -equiv -make_assert -flatten gold gate miter
stat
sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_BUFG
select -assert-count 6 t:CC_DFF
select -assert-max 2 t:CC_LUT1
select -assert-count 1 t:CC_LUT2
select -assert-max 14 t:CC_L2T4
select -assert-max 5 t:CC_L2T5
select -assert-max 1 t:CC_MX2
select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT1 t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 t:CC_MX2 %% t:* %D
design -load orig
equiv_opt -run :prove -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new
async2sync
miter -equiv -make_assert -flatten gold gate miter
stat
sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_BUFG
select -assert-count 6 t:CC_DFF
select -assert-count 2 t:CC_LUT2
select -assert-count 9 t:CC_L2T4
select -assert-count 6 t:CC_L2T5
select -assert-count 1 t:CC_MX2
select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 t:CC_MX2 %% t:* %D

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -27,3 +27,23 @@ cd latchsr # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_DLT
select -assert-max 2 t:CC_LUT3
select -assert-none t:CC_DLT t:CC_LUT3 %% t:* %D
design -load read
hierarchy -top latchsr
proc
equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchsr # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_DLT
select -assert-max 2 t:CC_L2T4
select -assert-none t:CC_DLT t:CC_L2T4 %% t:* %D
design -load read
hierarchy -top latchsr
proc
equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchsr # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_DLT
select -assert-max 2 t:CC_L2T4
select -assert-none t:CC_DLT t:CC_L2T4 %% t:* %D

View file

@ -1,6 +1,9 @@
read_verilog ../common/logic.v
hierarchy -top top
proc
design -save orig
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
@ -8,3 +11,23 @@ select -assert-max 1 t:CC_LUT1
select -assert-max 6 t:CC_LUT2
select -assert-max 2 t:CC_LUT4
select -assert-none t:CC_LUT1 t:CC_LUT2 t:CC_LUT4 %% t:* %D
design -load orig
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_LUT1
select -assert-count 6 t:CC_LUT2
select -assert-count 2 t:CC_L2T4
select -assert-none t:CC_LUT1 t:CC_LUT2 t:CC_L2T4 %% t:* %D
design -load orig
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_LUT1
select -assert-count 6 t:CC_LUT2
select -assert-count 2 t:CC_L2T4
select -assert-none t:CC_LUT1 t:CC_LUT2 t:CC_L2T4 %% t:* %D

View file

@ -11,3 +11,24 @@ cd luttrees # Constrain all select calls below inside the top module
select -assert-count 750 t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %%
select -assert-none t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% t:* %D
design -load read
hierarchy -top luttrees
proc
equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -nomx4 -nomx8 -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd luttrees # Constrain all select calls below inside the top module
select -assert-count 750 t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %%
select -assert-none t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% t:* %D
design -load read
hierarchy -top luttrees
proc
equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -nomx4 -nomx8 -luttree -abc_new # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd luttrees # Constrain all select calls below inside the top module
select -assert-count 750 t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %%
select -assert-none t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% t:* %D

View file

@ -31,3 +31,29 @@ select -assert-count 1 t:CC_BUFG
select -assert-max 18 t:CC_LUT4
select -assert-count 18 t:CC_DFF
select -assert-none t:CC_MULT t:CC_BUFG t:CC_LUT4 t:CC_DFF %% t:* %D
design -load read
hierarchy -top mul_unsigned_sync
proc
equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mul_unsigned_sync # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_MULT
select -assert-count 1 t:CC_BUFG
select -assert-count 18 t:CC_LUT2
select -assert-count 18 t:CC_MX2
select -assert-count 18 t:CC_DFF
select -assert-none t:CC_MULT t:CC_BUFG t:CC_LUT2 t:CC_MX2 t:CC_DFF %% t:* %D
design -load read
hierarchy -top mul_unsigned_sync
proc
# equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check (fails)
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mul_unsigned_sync # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_MULT
select -assert-count 1 t:CC_BUFG
select -assert-count 18 t:CC_LUT2
select -assert-count 18 t:CC_MX2
select -assert-count 18 t:CC_DFF
select -assert-none t:CC_MULT t:CC_BUFG t:CC_LUT2 t:CC_MX2 t:CC_DFF %% t:* %D

View file

@ -12,6 +12,25 @@ select -assert-max 2 t:CC_LUT4
select -assert-max 1 t:CC_MX2
select -assert-none t:CC_LUT2 t:CC_LUT4 t:CC_MX2 %% t:* %D
design -load read
hierarchy -top mux4
proc
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux4 # Constrain all select calls below inside the top module
select -assert-count 3 t:CC_MX2
select -assert-none t:CC_MX2 %% t:* %D
design -load read
hierarchy -top mux4
proc
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux4 # Constrain all select calls below inside the top module
select -assert-count 1 t:CC_LUT1
select -assert-count 3 t:CC_MX2
select -assert-none t:CC_LUT1 t:CC_MX2 %% t:* %D
design -load read
hierarchy -top mux8
proc
@ -22,3 +41,21 @@ select -assert-max 1 t:CC_LUT3
select -assert-max 5 t:CC_LUT4
select -assert-max 1 t:CC_MX2
select -assert-none t:CC_LUT3 t:CC_LUT4 t:CC_MX2 %% t:* %D
design -load read
hierarchy -top mux8
proc
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux8 # Constrain all select calls below inside the top module
select -assert-count 7 t:CC_MX2
select -assert-none t:CC_MX2 %% t:* %D
design -load read
hierarchy -top mux8
proc
equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -abc_new # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux8 # Constrain all select calls below inside the top module
select -assert-count 7 t:CC_MX2
select -assert-none t:CC_MX2 %% t:* %D

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

52
tests/arch/generate_mk.py Normal file
View file

@ -0,0 +1,52 @@
#!/usr/bin/env python3
from pathlib import Path
import sys
sys.path.append("..")
import gen_tests_makefile
techlibs_dir = Path("../../techlibs")
# Architecture-specific defines
defines = {
"ice40": ["ICE40_HX", "ICE40_LP", "ICE40_U"]
}
def archs():
# Loop over architectures
for arch in techlibs_dir.iterdir():
if not arch.is_dir():
continue
arch_name = arch.name
for path in arch.rglob("cells_sim.v"):
rel_parts = path.relative_to(techlibs_dir).parts
target_base = "_".join(rel_parts[-len(rel_parts):]).replace(".v", "")
path_str = str(path)
if arch_name in defines:
for defn in defines[arch_name]:
target_name = f"{target_base}_{defn}"
cmd = f"iverilog -t null -I{arch} -D{defn} -DNO_ICE40_DEFAULT_ASSIGNMENTS {path_str}"
gen_tests_makefile.generate_target(target_name, cmd)
else:
target_name = f"{target_base}"
cmd = f"iverilog -t null -I{arch} -g2005-sv {path_str}"
gen_tests_makefile.generate_target(target_name, cmd)
def common():
for path in ["../../techlibs/common/simcells.v", "../../techlibs/common/simlib.v"]:
path_obj = Path(path)
target_name = path_obj.stem
cmd = f"iverilog -t null {path}"
gen_tests_makefile.generate_target(target_name, cmd)
def main():
def callback():
archs()
common()
gen_tests_makefile.generate_custom(callback)
if __name__ == "__main__":
main()

View file

@ -0,0 +1,31 @@
read_verilog << EOT
`default_nettype none
module top (
input wire clk,
input wire [9:0] rd_addr,
output reg [15:0] rd_data,
input wire [9:0] wr_addr,
input wire [15:0] wr_data,
input wire wr_en
);
(* ram_style = "block" *) reg [15:0] mem [0:1023];
// Read port — separate always block
always @(posedge clk) begin
rd_data <= mem[rd_addr];
end
// Write port — separate always block
always @(posedge clk) begin
if (wr_en)
mem[wr_addr] <= wr_data;
end
endmodule
EOT
synth_gowin -top top
splitnets
select -assert-any top/mem.0.0 %ci*:+DPX9B[ADA]:+DFF:+IBUF i:wr_en %i

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -0,0 +1,25 @@
read_verilog ../common/latches.v
design -save read
hierarchy -top latchp
proc
equiv_opt -async2sync -assert -map +/gowin/cells_sim.v synth_gowin # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchp # Constrain all select calls below inside the top module
select -assert-count 1 t:DL
select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:DL t:IBUF t:OBUF %% t:* %D
design -load read
hierarchy -top latchn
proc
equiv_opt -async2sync -assert -map +/gowin/cells_sim.v synth_gowin # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchn # Constrain all select calls below inside the top module
select -assert-count 1 t:DLN
select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:DLN t:IBUF t:OBUF %% t:* %D

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -12,5 +12,5 @@ cd fsm # Constrain all select calls below inside the top module
select -assert-count 4 t:SB_DFF
select -assert-count 2 t:SB_DFFESR
select -assert-max 15 t:SB_LUT4
select -assert-max 16 t:SB_LUT4
select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -74,6 +74,7 @@ EOT
techmap -wb -D EQUIV -autoproc -map +/ice40/cells_sim.v
async2sync
equiv_make top ref equiv
select -assert-any -module equiv t:$equiv
equiv_induct

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,9 @@
#!/usr/bin/env python3
import sys
sys.path.append("../../..")
import gen_tests_makefile
import mem_gen
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,5 +0,0 @@
#!/usr/bin/env bash
set -eu
python3 mem_gen.py
source ../../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash

View file

@ -1,30 +0,0 @@
#!/usr/bin/env bash
source ../common-env.sh
set -e
declare -A defines=( ["ice40"]="ICE40_HX ICE40_LP ICE40_U" )
echo "Running syntax check on arch sim models"
for arch in ../../techlibs/*; do
find $arch -name cells_sim.v | while read path; do
arch_name=$(basename -- $arch)
if [ "${defines[$arch_name]}" ]; then
for def in ${defines[$arch_name]}; do
echo -n "Test $path -D$def ->"
iverilog -t null -I$arch -D$def -DNO_ICE40_DEFAULT_ASSIGNMENTS $path
echo " ok"
done
else
echo -n "Test $path ->"
iverilog -t null -I$arch -g2005-sv $path
echo " ok"
fi
done
done
for path in "../../techlibs/common/simcells.v" "../../techlibs/common/simlib.v"; do
echo -n "Test $path ->"
iverilog -t null $path
echo " ok"
done

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("../..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts", "--bash", "--yosys-args", "-w 'Yosys has only limited support for tri-state logic at the moment.'" ])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,197 @@
read_verilog <<EOT
module add3(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add5(
input [11:0] a, b, c, d, e,
output [11:0] y
);
assign y = a + b + c + d + e;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add8(
input [15:0] a, b, c, d, e, f, g, h,
output [15:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add16(
input [15:0] a0, a1, a2, a3, a4, a5, a6, a7,
input [15:0] a8, a9, a10, a11, a12, a13, a14, a15,
output [15:0] y
);
assign y = a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7
+ a8 + a9 + a10 + a11 + a12 + a13 + a14 + a15;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 14 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog -icells <<EOT
module alu_add3(
input [7:0] a, b, c,
output [7:0] y
);
wire [7:0] tmp, x1, x2, co1, co2;
// a + b
$alu #(.A_WIDTH(8), .B_WIDTH(8), .Y_WIDTH(8), .A_SIGNED(0), .B_SIGNED(0))
alu1 (.A(a), .B(b), .BI(1'b0), .CI(1'b0), .Y(tmp), .X(x1), .CO(co1));
// tmp + c
$alu #(.A_WIDTH(8), .B_WIDTH(8), .Y_WIDTH(8), .A_SIGNED(0), .B_SIGNED(0))
alu2 (.A(tmp), .B(c), .BI(1'b0), .CI(1'b0), .Y(y), .X(x2), .CO(co2));
endmodule
EOT
hierarchy -auto-top
select -assert-count 2 t:$alu
arith_tree
opt_clean
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
design -reset
read_verilog -icells <<EOT
module alu_add4(
input [7:0] a, b, c, d,
output [7:0] y
);
wire [7:0] tmp1, tmp2, x1, x2, x3, co1, co2, co3;
// a + b
$alu #(.A_WIDTH(8), .B_WIDTH(8), .Y_WIDTH(8), .A_SIGNED(0), .B_SIGNED(0))
alu1 (.A(a), .B(b), .BI(1'b0), .CI(1'b0), .Y(tmp1), .X(x1), .CO(co1));
// c + d
$alu #(.A_WIDTH(8), .B_WIDTH(8), .Y_WIDTH(8), .A_SIGNED(0), .B_SIGNED(0))
alu2 (.A(c), .B(d), .BI(1'b0), .CI(1'b0), .Y(tmp2), .X(x2), .CO(co2));
// tmp1 + tmp2
$alu #(.A_WIDTH(8), .B_WIDTH(8), .Y_WIDTH(8), .A_SIGNED(0), .B_SIGNED(0))
alu3 (.A(tmp1), .B(tmp2), .BI(1'b0), .CI(1'b0), .Y(y), .X(x3), .CO(co3));
endmodule
EOT
hierarchy -auto-top
select -assert-count 3 t:$alu
arith_tree
opt_clean
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
design -reset
read_verilog -icells <<EOT
module alu_add5(
input [11:0] a, b, c, d, e,
output [11:0] y
);
wire [11:0] tmp1, tmp2, tmp3, x1, x2, x3, x4, co1, co2, co3, co4;
// a + b
$alu #(.A_WIDTH(12), .B_WIDTH(12), .Y_WIDTH(12), .A_SIGNED(0), .B_SIGNED(0))
alu1 (.A(a), .B(b), .BI(1'b0), .CI(1'b0), .Y(tmp1), .X(x1), .CO(co1));
// c + d
$alu #(.A_WIDTH(12), .B_WIDTH(12), .Y_WIDTH(12), .A_SIGNED(0), .B_SIGNED(0))
alu2 (.A(c), .B(d), .BI(1'b0), .CI(1'b0), .Y(tmp2), .X(x2), .CO(co2));
// tmp1 + tmp2
$alu #(.A_WIDTH(12), .B_WIDTH(12), .Y_WIDTH(12), .A_SIGNED(0), .B_SIGNED(0))
alu3 (.A(tmp1), .B(tmp2), .BI(1'b0), .CI(1'b0), .Y(tmp3), .X(x3), .CO(co3));
// tmp3 + e
$alu #(.A_WIDTH(12), .B_WIDTH(12), .Y_WIDTH(12), .A_SIGNED(0), .B_SIGNED(0))
alu4 (.A(tmp3), .B(e), .BI(1'b0), .CI(1'b0), .Y(y), .X(x4), .CO(co4));
endmodule
EOT
hierarchy -auto-top
select -assert-count 4 t:$alu
arith_tree
opt_clean
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
design -reset
# Test $macc cells (alumacc+opt output)
read_verilog <<EOT
module macc_add3(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
arith_tree
opt_clean
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$macc t:$macc_v2 %u
design -reset
read_verilog <<EOT
module macc_add5(
input [11:0] a, b, c, d, e,
output [11:0] y
);
assign y = a + b + c + d + e;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
arith_tree
opt_clean
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$macc t:$macc_v2 %u
design -reset
read_verilog <<EOT
module macc_add8(
input [15:0] a, b, c, d, e, f, g, h,
output [15:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
arith_tree
opt_clean
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$macc t:$macc_v2 %u
design -reset

View file

@ -0,0 +1,107 @@
read_verilog <<EOT
module equiv_macc_add3(
input [3:0] a, b, c,
output [3:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
equiv_opt arith_tree
design -load postopt
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_macc_add4(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
equiv_opt arith_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_macc_add8(
input [3:0] a, b, c, d, e, f, g, h,
output [3:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
equiv_opt arith_tree
design -load postopt
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_macc_signed(
input signed [3:0] a, b, c, d,
output signed [5:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
equiv_opt arith_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_macc_sub_mixed(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a + b - c + d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
equiv_opt arith_tree
design -load postopt
select -assert-min 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_macc_sub_all(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a - b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
equiv_opt arith_tree
design -load postopt
select -assert-min 1 t:$fa
select -assert-count 1 t:$add
design -reset

View file

@ -0,0 +1,407 @@
read_verilog <<EOT
module add_1bit(
input a, b, c,
output [1:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_1bit_wide(
input a, b, c, d,
output [3:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_wide_out(
input [7:0] a, b, c, d,
output [31:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_mixed(
input [7:0] a,
input [3:0] b,
input [15:0] c,
input [7:0] d,
output [15:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_signed(
input signed [7:0] a, b, c, d,
output signed [9:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_repeated(
input [7:0] a,
output [7:0] y
);
assign y = a + a + a + a;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_const(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a + b + c + 8'd42;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_two(
input [7:0] a, b, c, d, e, f, g, h,
output [7:0] y1, y2
);
assign y1 = a + b + c + d;
assign y2 = e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 4 t:$fa
select -assert-count 2 t:$add
design -reset
read_verilog <<EOT
module fir_4tap(
input clk,
input [15:0] x, c0, c1, c2, c3,
output reg [31:0] y
);
reg [15:0] x1, x2, x3;
always @(posedge clk) begin
x1 <= x;
x2 <= x1;
x3 <= x2;
end
wire [31:0] sum = x*c0 + x1*c1 + x2*c2 + x3*c3;
always @(posedge clk) y <= sum;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module alu_add2(
input [7:0] a, b,
output [7:0] y
);
assign y = a + b;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
select -assert-none t:$fa
select -assert-none t:$add
select -assert-none t:$sub
select -assert-count 1 t:$alu
design -reset
read_verilog <<EOT
module alu_sub2(
input [7:0] a, b,
output [7:0] y
);
assign y = a - b;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
select -assert-none t:$fa
select -assert-none t:$add
select -assert-none t:$sub
select -assert-count 1 t:$alu
design -reset
read_verilog <<EOT
module alu_compare(
input [7:0] a, b,
output y
);
assign y = (a < b);
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
select -assert-none t:$fa
select -assert-none t:$add
select -assert-none t:$sub
select -assert-count 1 t:$alu
design -reset
read_verilog <<EOT
module macc_mul(
input [7:0] a, b, c,
output [15:0] y
);
assign y = a * b + c;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
arith_tree
opt_clean
select -assert-none t:$fa
select -assert-min 1 t:$macc t:$macc_v2 %u
design -reset
read_verilog <<EOT
module alu_fanout(
input [7:0] a, b, c,
output [7:0] mid, y
);
wire [7:0] ab = a + b;
assign mid = ab;
assign y = ab + c;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-none t:$fa
select -assert-count 2 t:$alu
design -reset
read_verilog <<EOT
module macc_2port(
input [7:0] a, b,
output [7:0] y
);
assign y = a + b;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
arith_tree
opt_clean
select -assert-none t:$fa
design -reset
read_verilog <<EOT
module macc_mixed_width(
input [7:0] a,
input [3:0] b,
input [15:0] c,
input [7:0] d,
output [15:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module macc_signed(
input signed [7:0] a, b, c, d,
output signed [9:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module fir_4tap_macc(
input clk,
input [15:0] x, c0, c1, c2, c3,
output reg [31:0] y
);
reg [15:0] x1, x2, x3;
always @(posedge clk) begin
x1 <= x;
x2 <= x1;
x3 <= x2;
end
wire [31:0] sum = x*c0 + x1*c1 + x2*c2 + x3*c3;
always @(posedge clk) y <= sum;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-min 1 t:$dff
design -reset
read_verilog <<EOT
module macc_mixed_sign(
input signed [7:0] a,
input [7:0] b,
input signed [7:0] c,
output signed [9:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module macc_wide32(
input [31:0] a, b, c, d,
output [31:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module passthrough(
input [7:0] a,
output [7:0] y
);
assign y = a;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
select -assert-none t:$fa
select -assert-none t:$add
select -assert-none t:$sub
select -assert-none t:$alu
design -reset
read_verilog <<EOT
module macc_mul_survives(
input [7:0] a, b, c, d,
output [15:0] y
);
assign y = a * b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
arith_tree
opt_clean
select -assert-none t:$fa
select -assert-min 1 t:$macc t:$macc_v2 %u
design -reset

View file

@ -0,0 +1,178 @@
read_verilog <<EOT
module equiv_add3(
input [3:0] a, b, c,
output [3:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_add4(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_add5(
input [3:0] a, b, c, d, e,
output [3:0] y
);
assign y = a + b + c + d + e;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_add8(
input [3:0] a, b, c, d, e, f, g, h,
output [3:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_signed(
input signed [3:0] a, b, c, d,
output signed [5:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_mixed(
input [1:0] a,
input [3:0] b,
input [5:0] c,
output [5:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_sub_3op(
input [3:0] a, b, c,
output [3:0] y
);
assign y = a - b + c;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_sub_mixed(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a + b - c + d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-min 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_sub_all(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a - b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-min 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_sub_signed(
input signed [3:0] a, b, c, d,
output signed [5:0] y
);
assign y = a + b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_double_neg(
input [3:0] a, b, c,
output [3:0] y
);
wire [3:0] ab = a - b;
assign y = c - ab;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt arith_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset

View file

@ -0,0 +1,46 @@
read_verilog <<EOT
module add8(
input [15:0] a, b, c, d, e, f, g, h,
output [15:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
arith_tree
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module macc_idempotent(
input [15:0] a, b, c, d, e, f, g, h,
output [15:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$sub
select -assert-none t:$alu
arith_tree
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$sub
select -assert-none t:$alu
design -reset

View file

@ -0,0 +1,77 @@
read_verilog <<EOT
module add2(
input [7:0] a, b,
output [7:0] y
);
assign y = a + b;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-none t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_fanout(
input [7:0] a, b, c,
output [7:0] mid, y
);
wire [7:0] ab = a + b;
assign mid = ab;
assign y = ab + c;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-none t:$fa
design -reset
read_verilog <<EOT
module sub2(
input [7:0] a, b,
output [7:0] y
);
assign y = a - b;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-none t:$fa
select -assert-count 1 t:$sub
design -reset
read_verilog <<EOT
module add_multi_const(
input [7:0] x,
output [7:0] y
);
assign y = 8'd1 + 8'd2 + 8'd3 + x;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-none t:$fa
select -assert-max 1 t:$add
design -reset
read_verilog <<EOT
module add_partial(
input [7:0] a, b, c, d, e,
output [7:0] mid, y
);
wire [7:0] ab = a + b;
assign mid = ab;
assign y = ab + c + d + e;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 2 t:$add
design -reset

View file

@ -0,0 +1,240 @@
read_verilog <<EOT
module sub_3op(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a - b + c;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-count 1 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_mixed(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a + b - c + d;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-count 1 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_all(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a - b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-count 3 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_5op(
input [11:0] a, b, c, d, e,
output [11:0] y
);
assign y = a - b + c - d + e;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 4 t:$fa
select -assert-count 1 t:$add
select -assert-count 2 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_signed(
input signed [7:0] a, b, c, d,
output signed [9:0] y
);
assign y = a + b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-count 2 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_double_neg(
input [7:0] a, b, c,
output [7:0] y
);
wire [7:0] ab = a - b;
assign y = c - ab;
endmodule
EOT
hierarchy -auto-top
proc
arith_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-count 1 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module macc_sub_3op(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a - b + c;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module macc_sub_mixed2(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a + b - c + d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module macc_sub_all(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a - b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module macc_sub_signed(
input signed [7:0] a, b, c, d,
output signed [9:0] y
);
assign y = a + b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt_clean
arith_tree
opt_clean
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$alu
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module macc_sub_mixed(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a + b - c + d;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
arith_tree
opt_clean
select -assert-none t:$macc t:$macc_v2 %u
select -assert-min 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module macc_const(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a + b + c + 8'd42;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
arith_tree
opt_clean
select -assert-none t:$macc t:$macc_v2 %u
select -assert-min 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module macc_two(
input [7:0] a, b, c, d, e, f, g, h,
output [7:0] y1, y2
);
assign y1 = a + b + c + d;
assign y2 = e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
alumacc
opt
arith_tree
opt_clean
select -assert-none t:$macc t:$macc_v2 %u
select -assert-count 4 t:$fa
select -assert-count 2 t:$add
design -reset

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts"])

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("..")
import gen_tests_makefile
gen_tests_makefile.generate_autotest("*.v", "-e")

View file

@ -1,15 +0,0 @@
#!/usr/bin/env bash
source ../common-env.sh
OPTIND=1
seed="" # default to no seed specified
while getopts "S:" opt
do
case "$opt" in
S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space
seed="SEED=$arg" ;;
esac
done
shift "$((OPTIND-1))"
exec ${MAKE:-make} -f ../tools/autotest.mk $seed EXTRA_FLAGS+="-e" *.v

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts"])

View file

@ -1,20 +0,0 @@
#!/usr/bin/env bash
set -e
{
echo "all::"
for x in *.ys; do
echo "all:: run-$x"
echo "run-$x:"
echo " @echo 'Running $x..'"
echo " @../../yosys -ql ${x%.ys}.log $x"
done
for s in *.sh; do
if [ "$s" != "run-test.sh" ]; then
echo "all:: run-$s"
echo "run-$s:"
echo " @echo 'Running $s..'"
echo " @bash $s"
fi
done
} > run-test.mk
exec ${MAKE:-make} -f run-test.mk

View file

@ -1,4 +1,3 @@
# Generated by Yosys
.model test
.inputs clk in_a_var[0] in_a_var[1] in_a_var[2] in_a_var[3] in_a_var[4] in_a_var[5] in_a_var[6] in_a_var[7] in_b_var[0] in_b_var[1] in_b_var[2] in_b_var[3] in_b_var[4] in_b_var[5] in_b_var[6] in_b_var[7]

View file

@ -1,2 +1,4 @@
read_blif gatesi.blif
write_blif -gatesi gatesi.blif.out
write_blif -gatesi gatesi.blif.out
! tail -n +2 gatesi.blif.out > gatesi.blif.out.tmp && mv gatesi.blif.out.tmp gatesi.blif.out
! diff gatesi.blif.out gatesi.blif.ok

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts"])

View file

@ -1,11 +0,0 @@
#!/usr/bin/env bash
source ../common-env.sh
set -e
for x in *.ys; do
echo "Running $x.."
../../yosys --no-version -ql ${x%.ys}.log $x
done
for x in *.blif; do
diff $x.out $x.ok
done

View file

@ -4,6 +4,10 @@ import argparse
import os
import sys
import random
import glob
sys.path.append("..")
import gen_tests_makefile
debug_mode = False
@ -287,9 +291,11 @@ if args.seed is not None:
else:
seed = (int(os.times()[4]*100) + os.getpid()) % 900000 + 100000
print("PRNG seed: %d" % seed)
print("bram PRNG seed: %d" % seed)
random.seed(seed)
os.makedirs("temp", exist_ok=True)
for k1 in range(args.count):
dsc_f = open("temp/brams_%02d.txt" % k1, "w")
sim_f = open("temp/brams_%02d.v" % k1, "w")
@ -303,3 +309,19 @@ for k1 in range(args.count):
for k2 in range(lenk2):
create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, random.randrange(2 if k2+1 < lenk2 else 1))
configs = sorted(set(
os.path.basename(f).replace("brams_", "").replace(".txt", "")
for f in glob.glob("temp/brams_*.txt")
))
def create_tests():
for i in configs:
for j in configs:
if i != j:
gen_tests_makefile.generate_cmd_test(
f"bram_{i}_{j}",
f"bash run-single.sh {i} {j}"
)
gen_tests_makefile.generate_custom(create_tests)

View file

@ -1,48 +0,0 @@
#!/usr/bin/env bash
source ../common-env.sh
# run this test many times:
# MAKE="make -j8" time bash -c 'for ((i=0; i<100; i++)); do echo "-- $i --"; bash run-test.sh || exit 1; done'
set -e
OPTIND=1
count=5
seed="" # default to no seed specified
debug=""
while getopts "c:dS:" opt
do
case "$opt" in
c) count="$OPTARG" ;;
d) debug="-d" ;;
S) seed="-S $OPTARG" ;;
esac
done
shift "$((OPTIND-1))"
rm -rf temp
mkdir -p temp
echo "generating tests.."
python3 generate.py $debug -c $count $seed
{
echo -n "all:"
for i in $( ls temp/brams_*.txt | sed 's,.*_,,; s,\..*,,;' ); do
for j in $( ls temp/brams_*.txt | sed 's,.*_,,; s,\..*,,;' | grep -v $i ); do
echo -n " temp/job_${i}_${j}.ok"
done; done
echo
for i in $( ls temp/brams_*.txt | sed 's,.*_,,; s,\..*,,;' ); do
for j in $( ls temp/brams_*.txt | sed 's,.*_,,; s,\..*,,;' | grep -v $i ); do
echo "temp/job_${i}_${j}.ok:"
echo " @bash run-single.sh ${i} ${j}"
echo " @echo 'Passed memory_bram test ${i}_${j}.'"
echo " @touch \$@"
done; done
} > temp/makefile
echo "running tests.."
${MAKE:-make} -f temp/makefile
exit 0

View file

@ -0,0 +1,8 @@
#!/usr/bin/env python3
import sys
sys.path.append("..")
import gen_tests_makefile
gen_tests_makefile.generate(["--yosys-scripts"])

View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
set -eu
source ../gen-tests-makefile.sh
generate_mk --yosys-scripts

View file

@ -1 +0,0 @@
export YOSYS_MAX_THREADS=4

Some files were not shown because too many files have changed in this diff Show more