aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
authorSergey <37293587+SergeyDegtyar@users.noreply.github.com>2019-10-01 11:04:32 +0300
committerGitHub <noreply@github.com>2019-10-01 11:04:32 +0300
commite092c4ae6b60cf67efd16efbfbf739895ad501c0 (patch)
tree939a5b94d14a11df511aa95482458b33a1f6139f /tests
parent1070f2e90b9ba37856932189ef09a0f2316d9a21 (diff)
parentd963e8c2c6207ad98d48dc528922ad58c030173f (diff)
downloadyosys-e092c4ae6b60cf67efd16efbfbf739895ad501c0.tar.gz
yosys-e092c4ae6b60cf67efd16efbfbf739895ad501c0.tar.bz2
yosys-e092c4ae6b60cf67efd16efbfbf739895ad501c0.zip
Merge branch 'master' into SergeyDegtyar/efinix
Diffstat (limited to 'tests')
-rw-r--r--tests/ice40/adffs.v20
-rw-r--r--tests/ice40/adffs.ys13
-rw-r--r--tests/ice40/div_mod.ys2
-rw-r--r--tests/ice40/macc.v34
-rw-r--r--tests/ice40/macc.ys22
-rwxr-xr-xtests/ice40/run-test.sh2
-rw-r--r--tests/opt/opt_expr.ys14
-rw-r--r--tests/rpc/.gitignore1
-rw-r--r--tests/rpc/design.v8
-rw-r--r--tests/rpc/exec.ys5
-rw-r--r--tests/rpc/frontend.py126
-rwxr-xr-xtests/rpc/run-test.sh6
-rw-r--r--tests/rpc/unix.ys6
-rw-r--r--tests/simple/peepopt.v13
-rwxr-xr-xtests/simple/run-test.sh2
-rwxr-xr-xtests/simple_abc9/run-test.sh2
-rw-r--r--tests/techmap/autopurge.ys62
-rw-r--r--tests/techmap/dff2dffs.ys50
-rw-r--r--tests/techmap/extractinv.ys41
-rw-r--r--tests/techmap/wireinit.ys108
-rw-r--r--tests/various/abc9.v4
-rw-r--r--tests/various/equiv_opt_multiclock.ys12
-rw-r--r--tests/various/hierarchy_defer.ys27
-rw-r--r--tests/various/peepopt.ys175
-rw-r--r--tests/xilinx/.gitignore1
-rw-r--r--tests/xilinx/dsp_simd.ys25
-rw-r--r--tests/xilinx/latches.v58
-rw-r--r--tests/xilinx/latches.ys15
-rw-r--r--tests/xilinx/macc.sh3
-rw-r--r--tests/xilinx/macc.v84
-rw-r--r--tests/xilinx/macc.ys31
-rw-r--r--tests/xilinx/macc_tb.v96
-rw-r--r--tests/xilinx/mul_unsigned.v30
-rw-r--r--tests/xilinx/mul_unsigned.ys10
34 files changed, 1053 insertions, 55 deletions
diff --git a/tests/ice40/adffs.v b/tests/ice40/adffs.v
index 93c8bf52c..09dc36001 100644
--- a/tests/ice40/adffs.v
+++ b/tests/ice40/adffs.v
@@ -22,29 +22,25 @@ module adffn
q <= d;
endmodule
-module dffsr
+module dffs
( input d, clk, pre, clr, output reg q );
initial begin
q = 0;
end
- always @( posedge clk, posedge pre, posedge clr )
- if ( clr )
- q <= 1'b0;
- else if ( pre )
+ always @( posedge clk, posedge pre )
+ if ( pre )
q <= 1'b1;
else
q <= d;
endmodule
-module ndffnsnr
+module ndffnr
( input d, clk, pre, clr, output reg q );
initial begin
q = 0;
end
- always @( negedge clk, negedge pre, negedge clr )
- if ( !clr )
- q <= 1'b0;
- else if ( !pre )
+ always @( negedge clk, negedge pre )
+ if ( !pre )
q <= 1'b1;
else
q <= d;
@@ -58,7 +54,7 @@ input a,
output b,b1,b2,b3
);
-dffsr u_dffsr (
+dffs u_dffs (
.clk (clk ),
.clr (clr),
.pre (pre),
@@ -66,7 +62,7 @@ dffsr u_dffsr (
.q (b )
);
-ndffnsnr u_ndffnsnr (
+ndffnr u_ndffnr (
.clk (clk ),
.clr (clr),
.pre (pre),
diff --git a/tests/ice40/adffs.ys b/tests/ice40/adffs.ys
index 14b251c5c..548060b66 100644
--- a/tests/ice40/adffs.ys
+++ b/tests/ice40/adffs.ys
@@ -1,12 +1,11 @@
read_verilog adffs.v
proc
-async2sync # converts async flops to a 'sync' variant clocked by a 'super'-clock
flatten
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
+equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_DFF
-select -assert-count 1 t:SB_DFFN
-select -assert-count 2 t:SB_DFFSR
-select -assert-count 7 t:SB_LUT4
-select -assert-none t:SB_DFF t:SB_DFFN t:SB_DFFSR t:SB_LUT4 %% t:* %D
+select -assert-count 1 t:SB_DFFNS
+select -assert-count 2 t:SB_DFFR
+select -assert-count 1 t:SB_DFFS
+select -assert-count 2 t:SB_LUT4
+select -assert-none t:SB_DFFNS t:SB_DFFR t:SB_DFFS t:SB_LUT4 %% t:* %D
diff --git a/tests/ice40/div_mod.ys b/tests/ice40/div_mod.ys
index 21cac7144..821d6c301 100644
--- a/tests/ice40/div_mod.ys
+++ b/tests/ice40/div_mod.ys
@@ -4,6 +4,6 @@ flatten
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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 62 t:SB_LUT4
+select -assert-count 59 t:SB_LUT4
select -assert-count 41 t:SB_CARRY
select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D
diff --git a/tests/ice40/macc.v b/tests/ice40/macc.v
index 6c3676c83..6f68e7500 100644
--- a/tests/ice40/macc.v
+++ b/tests/ice40/macc.v
@@ -13,13 +13,35 @@ reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c;
assign c = reg_tmp_c;
always @(posedge clk)
begin
-if(set)
-begin
-reg_tmp_c <= 0;
+ if(set)
+ begin
+ reg_tmp_c <= 0;
+ end
+ else
+ begin
+ reg_tmp_c <= a * b + c;
+ end
end
-else
+endmodule
+
+module top2(clk,a,b,c,hold);
+parameter A_WIDTH = 6 /*4*/;
+parameter B_WIDTH = 6 /*3*/;
+input hold;
+input clk;
+input signed [(A_WIDTH - 1):0] a;
+input signed [(B_WIDTH - 1):0] b;
+output signed [(A_WIDTH + B_WIDTH - 1):0] c;
+reg signed [A_WIDTH-1:0] reg_a;
+reg signed [B_WIDTH-1:0] reg_b;
+reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c;
+assign c = reg_tmp_c;
+always @(posedge clk)
begin
-reg_tmp_c <= a * b + c;
-end
+ if (!hold) begin
+ reg_a <= a;
+ reg_b <= b;
+ reg_tmp_c <= reg_a * reg_b + c;
+ end
end
endmodule
diff --git a/tests/ice40/macc.ys b/tests/ice40/macc.ys
index 0f4c19be5..fd30e79c5 100644
--- a/tests/ice40/macc.ys
+++ b/tests/ice40/macc.ys
@@ -1,13 +1,25 @@
read_verilog macc.v
proc
+design -save read
+
hierarchy -top top
-#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 -dsp # 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:SB_MAC16
+select -assert-none t:SB_MAC16 %% t:* %D
+
+design -load read
+hierarchy -top top2
-equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 -dsp
-async2sync
-equiv_opt -run prove: -assert null
+#equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+
+equiv_opt -run :prove -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+clk2fflogic
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -set-init-zero -seq 4 -verify -prove-asserts -show-ports miter
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
+cd top2 # Constrain all select calls below inside the top module
select -assert-count 1 t:SB_MAC16
select -assert-none t:SB_MAC16 %% t:* %D
diff --git a/tests/ice40/run-test.sh b/tests/ice40/run-test.sh
index 2c72ca3a9..46716f9a0 100755
--- a/tests/ice40/run-test.sh
+++ b/tests/ice40/run-test.sh
@@ -6,7 +6,7 @@ for x in *.ys; do
echo "all:: run-$x"
echo "run-$x:"
echo " @echo 'Running $x..'"
- echo " @../../yosys -ql ${x%.ys}.log $x -w 'Yosys has only limited support for tri-state logic at the moment.'"
+ echo " @../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
done
for s in *.sh; do
if [ "$s" != "run-test.sh" ]; then
diff --git a/tests/opt/opt_expr.ys b/tests/opt/opt_expr.ys
index ecc2c8da8..e0acead82 100644
--- a/tests/opt/opt_expr.ys
+++ b/tests/opt/opt_expr.ys
@@ -204,7 +204,7 @@ endmodule
EOT
check
-equiv_opt opt_expr -fine
+equiv_opt -assert opt_expr -fine
design -load postopt
select -assert-count 1 t:$alu r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
@@ -218,7 +218,7 @@ endmodule
EOT
check
-equiv_opt opt_expr -fine
+equiv_opt -assert opt_expr -fine
design -load postopt
select -assert-count 1 t:$alu r:A_WIDTH=8 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
@@ -232,7 +232,7 @@ endmodule
EOT
check
-equiv_opt opt_expr
+equiv_opt -assert opt_expr
design -load postopt
select -assert-count 1 t:$shiftx r:A_WIDTH=3 %i
@@ -246,7 +246,7 @@ endmodule
EOT
check
-equiv_opt opt_expr
+equiv_opt -assert opt_expr
design -load postopt
select -assert-count 1 t:$shiftx r:A_WIDTH=12 %i
@@ -260,7 +260,7 @@ endmodule
EOT
check
-equiv_opt opt_expr
+equiv_opt -assert opt_expr
design -load postopt
select -assert-count 1 t:$shift r:A_WIDTH=3 %i
@@ -274,7 +274,7 @@ endmodule
EOT
check
-equiv_opt opt_expr
+equiv_opt -assert opt_expr
design -load postopt
select -assert-count 1 t:$shift r:A_WIDTH=10 %i
@@ -288,6 +288,6 @@ endmodule
EOT
check
-equiv_opt opt_expr -keepdc
+equiv_opt -assert opt_expr -keepdc
design -load postopt
select -assert-count 1 t:$shift r:A_WIDTH=13 %i
diff --git a/tests/rpc/.gitignore b/tests/rpc/.gitignore
new file mode 100644
index 000000000..397b4a762
--- /dev/null
+++ b/tests/rpc/.gitignore
@@ -0,0 +1 @@
+*.log
diff --git a/tests/rpc/design.v b/tests/rpc/design.v
new file mode 100644
index 000000000..80f1dac1a
--- /dev/null
+++ b/tests/rpc/design.v
@@ -0,0 +1,8 @@
+module top(input [3:0] i, output [3:0] o);
+ python_inv #(
+ .width(4)
+ ) inv (
+ .i(i),
+ .o(o),
+ );
+endmodule
diff --git a/tests/rpc/exec.ys b/tests/rpc/exec.ys
new file mode 100644
index 000000000..b46009fb9
--- /dev/null
+++ b/tests/rpc/exec.ys
@@ -0,0 +1,5 @@
+connect_rpc -exec python3 frontend.py stdio
+read_verilog design.v
+hierarchy -top top
+flatten
+select -assert-count 1 t:$neg
diff --git a/tests/rpc/frontend.py b/tests/rpc/frontend.py
new file mode 100644
index 000000000..eff41738a
--- /dev/null
+++ b/tests/rpc/frontend.py
@@ -0,0 +1,126 @@
+def modules():
+ return ["python_inv"]
+
+def derive(module, parameters):
+ assert module == r"python_inv"
+ if parameters.keys() != {r"\width"}:
+ raise ValueError("Invalid parameters")
+ return "ilang", r"""
+module \impl
+ wire width {width:d} input 1 \i
+ wire width {width:d} output 2 \o
+ cell $neg $0
+ parameter \A_SIGNED 1'0
+ parameter \A_WIDTH 32'{width:b}
+ parameter \Y_WIDTH 32'{width:b}
+ connect \A \i
+ connect \Y \o
+ end
+end
+module \python_inv
+ wire width {width:d} input 1 \i
+ wire width {width:d} output 2 \o
+ cell \impl $0
+ connect \i \i
+ connect \o \o
+ end
+end
+""".format(width=parameters[r"\width"])
+
+# ----------------------------------------------------------------------------
+
+import json
+import argparse
+import sys, socket, os
+try:
+ import msvcrt, win32pipe, win32file
+except ImportError:
+ msvcrt = win32pipe = win32file = None
+
+def map_parameter(parameter):
+ if parameter["type"] == "unsigned":
+ return int(parameter["value"], 2)
+ if parameter["type"] == "signed":
+ width = len(parameter["value"])
+ value = int(parameter["value"], 2)
+ if value & (1 << (width - 1)):
+ value = -((1 << width) - value)
+ return value
+ if parameter["type"] == "string":
+ return parameter["value"]
+ if parameter["type"] == "real":
+ return float(parameter["value"])
+
+def call(input_json):
+ input = json.loads(input_json)
+ if input["method"] == "modules":
+ return json.dumps({"modules": modules()})
+ if input["method"] == "derive":
+ try:
+ frontend, source = derive(input["module"],
+ {name: map_parameter(value) for name, value in input["parameters"].items()})
+ return json.dumps({"frontend": frontend, "source": source})
+ except ValueError as e:
+ return json.dumps({"error": str(e)})
+
+def main():
+ parser = argparse.ArgumentParser()
+ modes = parser.add_subparsers(dest="mode")
+ mode_stdio = modes.add_parser("stdio")
+ if os.name == "posix":
+ mode_path = modes.add_parser("unix-socket")
+ if os.name == "nt":
+ mode_path = modes.add_parser("named-pipe")
+ mode_path.add_argument("path")
+ args = parser.parse_args()
+
+ if args.mode == "stdio":
+ while True:
+ input = sys.stdin.readline()
+ if not input: break
+ sys.stdout.write(call(input) + "\n")
+ sys.stdout.flush()
+
+ if args.mode == "unix-socket":
+ sock = socket.socket(socket.AF_UNIX, socket.SOCK_STREAM)
+ sock.bind(args.path)
+ try:
+ sock.listen(1)
+ conn, addr = sock.accept()
+ file = conn.makefile("rw")
+ while True:
+ input = file.readline()
+ if not input: break
+ file.write(call(input) + "\n")
+ file.flush()
+ finally:
+ sock.close()
+ os.unlink(args.path)
+
+ if args.mode == "named-pipe":
+ pipe = win32pipe.CreateNamedPipe(args.path, win32pipe.PIPE_ACCESS_DUPLEX,
+ win32pipe.PIPE_TYPE_BYTE|win32pipe.PIPE_READMODE_BYTE|win32pipe.PIPE_WAIT,
+ 1, 4096, 4096, 0, None)
+ win32pipe.ConnectNamedPipe(pipe, None)
+ try:
+ while True:
+ input = b""
+ while not input.endswith(b"\n"):
+ result, data = win32file.ReadFile(pipe, 4096)
+ assert result == 0
+ input += data
+ assert not b"\n" in input or input.endswith(b"\n")
+ output = (call(input.decode("utf-8")) + "\n").encode("utf-8")
+ length = len(output)
+ while length > 0:
+ result, done = win32file.WriteFile(pipe, output)
+ assert result == 0
+ length -= done
+ except win32file.error as e:
+ if e.args[0] == 109: # ERROR_BROKEN_PIPE
+ pass
+ else:
+ raise
+
+if __name__ == "__main__":
+ main()
diff --git a/tests/rpc/run-test.sh b/tests/rpc/run-test.sh
new file mode 100755
index 000000000..44ce7e674
--- /dev/null
+++ b/tests/rpc/run-test.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+set -e
+for x in *.ys; do
+ echo "Running $x.."
+ ../../yosys -ql ${x%.ys}.log $x
+done
diff --git a/tests/rpc/unix.ys b/tests/rpc/unix.ys
new file mode 100644
index 000000000..cc7ec14ab
--- /dev/null
+++ b/tests/rpc/unix.ys
@@ -0,0 +1,6 @@
+!python3 frontend.py unix-socket frontend.sock & sleep 0.1
+connect_rpc -path frontend.sock
+read_verilog design.v
+hierarchy -top top
+flatten
+select -assert-count 1 t:$neg
diff --git a/tests/simple/peepopt.v b/tests/simple/peepopt.v
deleted file mode 100644
index 1bf427897..000000000
--- a/tests/simple/peepopt.v
+++ /dev/null
@@ -1,13 +0,0 @@
-module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o);
-assign o = i[s*W+:W];
-endmodule
-
-module peepopt_shiftmul_1 (output y, input [2:0] w);
-assign y = 1'b1 >> (w * (3'b110));
-endmodule
-
-module peepopt_muldiv_0(input [1:0] i, output [1:0] o);
-wire [3:0] t;
-assign t = i * 3;
-assign o = t / 3;
-endmodule
diff --git a/tests/simple/run-test.sh b/tests/simple/run-test.sh
index 967ac49f2..f20fd0d30 100755
--- a/tests/simple/run-test.sh
+++ b/tests/simple/run-test.sh
@@ -12,7 +12,7 @@ done
shift "$((OPTIND-1))"
# check for Icarus Verilog
-if ! which iverilog > /dev/null ; then
+if ! command -v iverilog > /dev/null ; then
echo "$0: Error: Icarus Verilog 'iverilog' not found."
exit 1
fi
diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh
index 8df6994e3..0d4262005 100755
--- a/tests/simple_abc9/run-test.sh
+++ b/tests/simple_abc9/run-test.sh
@@ -12,7 +12,7 @@ done
shift "$((OPTIND-1))"
# check for Icarus Verilog
-if ! which iverilog > /dev/null ; then
+if ! command -v iverilog > /dev/null ; then
echo "$0: Error: Icarus Verilog 'iverilog' not found."
exit 1
fi
diff --git a/tests/techmap/autopurge.ys b/tests/techmap/autopurge.ys
new file mode 100644
index 000000000..1eb99ec37
--- /dev/null
+++ b/tests/techmap/autopurge.ys
@@ -0,0 +1,62 @@
+# https://github.com/YosysHQ/yosys/issues/1381
+read_verilog <<EOT
+module sub(input i, output o, (* techmap_autopurge *) input j);
+foobar f(i, o, j);
+endmodule
+EOT
+design -stash techmap
+
+read_verilog <<EOT
+(* blackbox *)
+module sub(input i, output o, input j);
+endmodule
+
+(* blackbox *)
+module foobar(input i, output o, input j);
+endmodule
+
+module top(input i, output o);
+sub s0(i, o);
+endmodule
+EOT
+
+techmap -map %techmap
+hierarchy
+check -assert
+
+# https://github.com/YosysHQ/yosys/issues/1391
+design -reset
+read_verilog <<EOT
+module sub(input i, output o, (* techmap_autopurge *) input [1:0] j);
+foobar f(i, o, j);
+endmodule
+EOT
+design -stash techmap
+
+read_verilog <<EOT
+(* blackbox *)
+module sub(input i, output o, input j);
+endmodule
+
+(* blackbox *)
+module foobar(input i, output o, input j);
+endmodule
+
+module top(input i, output o);
+sub s0(i, o);
+endmodule
+EOT
+
+techmap -map %techmap
+hierarchy
+check -assert
+
+read_verilog -overwrite <<EOT
+module top(input i, output o);
+wire j;
+sub s0(i, o, j);
+endmodule
+EOT
+
+techmap -map %techmap
+hierarchy
diff --git a/tests/techmap/dff2dffs.ys b/tests/techmap/dff2dffs.ys
new file mode 100644
index 000000000..13f1a3cf3
--- /dev/null
+++ b/tests/techmap/dff2dffs.ys
@@ -0,0 +1,50 @@
+read_verilog << EOT
+module top(...);
+input clk;
+input d;
+input sr;
+output reg q0, q1, q2, q3, q4, q5;
+
+initial q0 = 1'b0;
+initial q1 = 1'b0;
+initial q2 = 1'b1;
+initial q3 = 1'b1;
+initial q4 = 1'bx;
+initial q5 = 1'bx;
+
+always @(posedge clk) begin
+ q0 <= sr ? 1'b0 : d;
+ q1 <= sr ? 1'b1 : d;
+ q2 <= sr ? 1'b0 : d;
+ q3 <= sr ? 1'b1 : d;
+ q4 <= sr ? 1'b0 : d;
+ q5 <= sr ? 1'b1 : d;
+end
+
+endmodule
+EOT
+
+proc
+simplemap
+design -save ref
+
+dff2dffs
+clean
+
+select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q1 %x t:$__DFFS_PP1_ %i
+select -assert-count 1 w:q2 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i
+select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i
+
+design -load ref
+dff2dffs -match-init
+clean
+
+select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i
+select -assert-count 0 w:q1 %x t:$__DFFS_PP1_ %i
+select -assert-count 0 w:q2 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i
+select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i
diff --git a/tests/techmap/extractinv.ys b/tests/techmap/extractinv.ys
new file mode 100644
index 000000000..6146f829a
--- /dev/null
+++ b/tests/techmap/extractinv.ys
@@ -0,0 +1,41 @@
+read_verilog << EOT
+
+module ff4(...);
+parameter [0:0] CLK_INV = 1'b0;
+parameter [3:0] DATA_INV = 4'b0000;
+(* invertible_pin = "CLK_INV" *)
+input clk;
+(* invertible_pin = "DATA_INV" *)
+input [3:0] d;
+output [3:0] q;
+endmodule
+
+module inv(...);
+output o;
+input i;
+endmodule
+
+module top(...);
+input d0, d1, d2, d3;
+input clk;
+output q;
+ff4 #(.DATA_INV(4'h5)) ff_inst (.clk(clk), .d({d3, d2, d1, d0}), .q(q));
+endmodule
+
+EOT
+
+extractinv -inv inv o:i
+clean
+
+select -assert-count 2 top/t:inv
+select -assert-count 2 top/t:inv top/t:ff4 %ci:+[d] %ci:+[o] %i
+
+select -assert-count 1 top/t:inv top/w:d0 %co:+[i] %i
+select -assert-count 0 top/t:inv top/w:d1 %co:+[i] %i
+select -assert-count 1 top/t:inv top/w:d2 %co:+[i] %i
+select -assert-count 0 top/t:inv top/w:d3 %co:+[i] %i
+
+select -assert-count 0 top/t:ff4 top/w:d0 %co:+[d] %i
+select -assert-count 1 top/t:ff4 top/w:d1 %co:+[d] %i
+select -assert-count 0 top/t:ff4 top/w:d2 %co:+[d] %i
+select -assert-count 1 top/t:ff4 top/w:d3 %co:+[d] %i
diff --git a/tests/techmap/wireinit.ys b/tests/techmap/wireinit.ys
new file mode 100644
index 000000000..89afaafb5
--- /dev/null
+++ b/tests/techmap/wireinit.ys
@@ -0,0 +1,108 @@
+read_verilog <<EOT
+(* techmap_celltype = "$_DFF_P_" *)
+module ffmap(...);
+input D;
+input C;
+output Q;
+parameter [0:0] _TECHMAP_WIREINIT_Q_ = 1'bx;
+
+ffbb #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_(.D(D), .Q(Q), .C(C));
+
+wire _TECHMAP_FAIL_ = _TECHMAP_WIREINIT_Q_ === 1'b1;
+
+wire _TECHMAP_REMOVEINIT_Q_ = 1'b1;
+
+endmodule
+EOT
+design -stash map
+
+read_verilog <<EOT
+(* techmap_celltype = "$_DFF_P_" *)
+module ffmap(...);
+input D;
+input C;
+output Q;
+parameter [0:0] _TECHMAP_WIREINIT_Q_ = 1'bx;
+
+ffbb #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_(.D(D), .Q(Q), .C(C));
+
+wire _TECHMAP_FAIL_ = _TECHMAP_WIREINIT_Q_ === 1'b1;
+
+wire _TECHMAP_REMOVEINIT_Q_ = 1'b0;
+
+endmodule
+EOT
+design -stash map_noremove
+
+read_verilog <<EOT
+module ffbb (...);
+parameter [0:0] INIT = 1'bx;
+input D, C;
+output Q;
+endmodule
+
+module top(...);
+input clk;
+input d;
+output reg q0 = 0;
+output reg q1 = 1;
+output reg qq0 = 0;
+output reg qx;
+
+always @(posedge clk) begin
+ q0 <= d;
+ q1 <= d;
+ qq0 <= q0;
+ qx <= d;
+end
+endmodule
+EOT
+
+design -save ref
+
+hierarchy -auto-top
+proc
+simplemap
+techmap -map %map
+clean
+# Make sure the parameter was used properly.
+select -assert-count 3 top/t:ffbb
+select -set ff0 top/w:q0 %ci t:ffbb %i
+select -set ffq0 top/w:qq0 %ci t:ffbb %i
+select -set ffx top/w:qx %ci t:ffbb %i
+select -assert-count 1 @ff0
+select -assert-count 1 @ffq0
+select -assert-count 1 @ffx
+select -assert-count 1 @ff0 r:INIT=1'b0 %i
+select -assert-count 1 @ffq0 r:INIT=1'b0 %i
+select -assert-count 1 @ffx r:INIT=1'bx %i
+select -assert-count 0 top/w:q1 %ci t:ffbb %i
+# Make sure the init values are dropped from the wires iff mapping was performed.
+select -assert-count 0 top/w:q0 a:init %i
+select -assert-count 0 top/w:qq0 a:init %i
+select -assert-count 1 top/w:q1 a:init=1'b1 %i
+select -assert-count 0 top/w:qx a:init %i
+
+design -load ref
+hierarchy -auto-top
+proc
+simplemap
+techmap -map %map_noremove
+clean
+# Make sure the parameter was used properly.
+select -assert-count 3 top/t:ffbb
+select -set ff0 top/w:q0 %ci t:ffbb %i
+select -set ffq0 top/w:qq0 %ci t:ffbb %i
+select -set ffx top/w:qx %ci t:ffbb %i
+select -assert-count 1 @ff0
+select -assert-count 1 @ffq0
+select -assert-count 1 @ffx
+select -assert-count 1 @ff0 r:INIT=1'b0 %i
+select -assert-count 1 @ffq0 r:INIT=1'b0 %i
+select -assert-count 1 @ffx r:INIT=1'bx %i
+select -assert-count 0 top/w:q1 %ci t:ffbb %i
+# Make sure the init values are not dropped from the wires.
+select -assert-count 1 top/w:q0 a:init=1'b0 %i
+select -assert-count 1 top/w:qq0 a:init=1'b0 %i
+select -assert-count 1 top/w:q1 a:init=1'b1 %i
+select -assert-count 0 top/w:qx a:init %i
diff --git a/tests/various/abc9.v b/tests/various/abc9.v
index a08b613a8..30ebd4e26 100644
--- a/tests/various/abc9.v
+++ b/tests/various/abc9.v
@@ -5,5 +5,7 @@ always @*
endmodule
module abc9_test028(input i, output o);
-unknown u(~i, o);
+wire w;
+unknown u(~i, w);
+unknown2 u2(w, o);
endmodule
diff --git a/tests/various/equiv_opt_multiclock.ys b/tests/various/equiv_opt_multiclock.ys
new file mode 100644
index 000000000..81e36d018
--- /dev/null
+++ b/tests/various/equiv_opt_multiclock.ys
@@ -0,0 +1,12 @@
+read_verilog <<EOT
+module top(input clk, pre, d, output reg q);
+ always @(posedge clk, posedge pre)
+ if (pre)
+ q <= 1'b1;
+ else
+ q <= d;
+endmodule
+EOT
+
+prep
+equiv_opt -assert -multiclock -map +/simcells.v synth
diff --git a/tests/various/hierarchy_defer.ys b/tests/various/hierarchy_defer.ys
new file mode 100644
index 000000000..70f5b70a3
--- /dev/null
+++ b/tests/various/hierarchy_defer.ys
@@ -0,0 +1,27 @@
+read -noverific
+read -vlog2k <<EOT
+module first;
+endmodule
+
+(* top *)
+module top(input i, output o);
+sub s0(i, o);
+endmodule
+
+(* constant_expression=1+1?2*2:3/3 *)
+module sub(input i, output o);
+assign o = ~i;
+endmodule
+EOT
+design -save read
+
+hierarchy -auto-top
+select -assert-any top
+select -assert-any sub
+select -assert-none foo
+
+design -load read
+hierarchy
+select -assert-any top
+select -assert-any sub
+select -assert-none foo
diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
new file mode 100644
index 000000000..6bca62e2b
--- /dev/null
+++ b/tests/various/peepopt.ys
@@ -0,0 +1,175 @@
+read_verilog <<EOT
+module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o);
+assign o = i[s*W+:W];
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$shiftx
+select -assert-count 0 t:$shiftx t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w);
+assign y = 1'b1 >> (w * (3'b110));
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$shr
+select -assert-count 1 t:$mul
+select -assert-count 0 t:$shr t:$mul %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_shiftmul_2 (input [11:0] D, input [1:0] S, output [11:0] Y);
+ assign Y = D >> (S*3);
+endmodule
+EOT
+
+prep
+design -save gold
+peepopt
+design -stash gate
+
+design -import gold -as gold peepopt_shiftmul_2
+design -import gate -as gate peepopt_shiftmul_2
+
+miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter
+sat -show-public -enable_undef -prove-asserts miter
+cd gate
+select -assert-count 1 t:$shr
+select -assert-count 1 t:$mul
+select -assert-count 0 t:$shr t:$mul %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_muldiv_0(input [1:0] i, output [1:0] o);
+wire [3:0] t;
+assign t = i * 3;
+assign o = t / 3;
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 0 t:*
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o);
+ always @(posedge clk) if (ce) o <= i;
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o);
+ always @(posedge clk) if (ce) o <= i;
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+###################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o);
+ always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+###################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o);
+ always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+select -assert-count 1 t:$dff r:WIDTH=5 %i
+select -assert-count 1 t:$mux r:WIDTH=5 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o);
+ always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i;
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+wreduce
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 2 t:$mux
+select -assert-count 2 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
+ always @(posedge clk) begin
+ if (ce) o <= i;
+ if (!rstn) o <= 4'b1111;
+ end
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+wreduce
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 2 t:$mux
+select -assert-count 2 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D
diff --git a/tests/xilinx/.gitignore b/tests/xilinx/.gitignore
index b48f808a1..54733fb71 100644
--- a/tests/xilinx/.gitignore
+++ b/tests/xilinx/.gitignore
@@ -1,3 +1,4 @@
/*.log
/*.out
/run-test.mk
+/*_uut.v
diff --git a/tests/xilinx/dsp_simd.ys b/tests/xilinx/dsp_simd.ys
new file mode 100644
index 000000000..956952327
--- /dev/null
+++ b/tests/xilinx/dsp_simd.ys
@@ -0,0 +1,25 @@
+read_verilog <<EOT
+module simd(input [12*4-1:0] a, input [12*4-1:0] b, (* use_dsp="simd" *) output [7*12-1:0] o12, (* use_dsp="simd" *) output [2*24-1:0] o24);
+generate
+ genvar i;
+ // 4 x 12-bit adder
+ for (i = 0; i < 4; i++)
+ assign o12[i*12+:12] = a[i*12+:12] + b[i*12+:12];
+ // 2 x 24-bit subtract
+ for (i = 0; i < 2; i++)
+ assign o24[i*24+:24] = a[i*24+:24] - b[i*24+:24];
+endgenerate
+reg [3*12-1:0] ro;
+always @* begin
+ ro[0*12+:12] = a[0*10+:10] + b[0*10+:10];
+ ro[1*12+:12] = a[1*10+:10] + b[1*10+:10];
+ ro[2*12+:12] = a[2*8+:8] + b[2*8+:8];
+end
+assign o12[4*12+:3*12] = ro;
+endmodule
+EOT
+
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx
+design -load postopt
+select -assert-count 3 t:DSP48E1
diff --git a/tests/xilinx/latches.v b/tests/xilinx/latches.v
new file mode 100644
index 000000000..83bad7f35
--- /dev/null
+++ b/tests/xilinx/latches.v
@@ -0,0 +1,58 @@
+module latchp
+ ( input d, en, output reg q );
+ always @*
+ if ( en )
+ q <= d;
+endmodule
+
+module latchn
+ ( input d, en, output reg q );
+ always @*
+ if ( !en )
+ q <= d;
+endmodule
+
+module latchsr
+ ( input d, en, clr, pre, output reg q );
+ always @*
+ if ( clr )
+ q <= 1'b0;
+ else if ( pre )
+ q <= 1'b1;
+ else if ( en )
+ q <= d;
+endmodule
+
+
+module top (
+input clk,
+input clr,
+input pre,
+input a,
+output b,b1,b2
+);
+
+
+latchp u_latchp (
+ .en (clk ),
+ .d (a ),
+ .q (b )
+ );
+
+
+latchn u_latchn (
+ .en (clk ),
+ .d (a ),
+ .q (b1 )
+ );
+
+
+latchsr u_latchsr (
+ .en (clk ),
+ .clr (clr),
+ .pre (pre),
+ .d (a ),
+ .q (b2 )
+ );
+
+endmodule
diff --git a/tests/xilinx/latches.ys b/tests/xilinx/latches.ys
new file mode 100644
index 000000000..ac1102896
--- /dev/null
+++ b/tests/xilinx/latches.ys
@@ -0,0 +1,15 @@
+read_verilog latches.v
+
+proc
+flatten
+equiv_opt -assert -run :prove -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+async2sync
+equiv_opt -assert -run prove: -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+
+design -load preopt
+synth_xilinx
+cd top
+select -assert-count 1 t:LUT1
+select -assert-count 2 t:LUT3
+select -assert-count 3 t:LDCE
+select -assert-none t:LUT1 t:LUT3 t:LDCE %% t:* %D
diff --git a/tests/xilinx/macc.sh b/tests/xilinx/macc.sh
new file mode 100644
index 000000000..86e4c2bb6
--- /dev/null
+++ b/tests/xilinx/macc.sh
@@ -0,0 +1,3 @@
+../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" macc.v -o macc_uut.v
+iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../techlibs/xilinx/cells_sim.v
+vvp -N ./test_macc
diff --git a/tests/xilinx/macc.v b/tests/xilinx/macc.v
new file mode 100644
index 000000000..e36b2bab1
--- /dev/null
+++ b/tests/xilinx/macc.v
@@ -0,0 +1,84 @@
+// Signed 40-bit streaming accumulator with 16-bit inputs
+// File: HDL_Coding_Techniques/multipliers/multipliers4.v
+//
+// Source:
+// https://www.xilinx.com/support/documentation/sw_manuals/xilinx2014_2/ug901-vivado-synthesis.pdf p.90
+//
+module macc # (parameter SIZEIN = 16, SIZEOUT = 40) (
+ input clk, ce, sload,
+ input signed [SIZEIN-1:0] a, b,
+ output signed [SIZEOUT-1:0] accum_out
+);
+// Declare registers for intermediate values
+reg signed [SIZEIN-1:0] a_reg, b_reg;
+reg sload_reg;
+reg signed [2*SIZEIN-1:0] mult_reg;
+reg signed [SIZEOUT-1:0] adder_out, old_result;
+always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch
+ if (sload_reg)
+ old_result <= 0;
+ else
+ // 'sload' is now active (=low) and opens the accumulation loop.
+ // The accumulator takes the next multiplier output in
+ // the same cycle.
+ old_result <= adder_out;
+end
+
+always @(posedge clk)
+ if (ce)
+ begin
+ a_reg <= a;
+ b_reg <= b;
+ mult_reg <= a_reg * b_reg;
+ sload_reg <= sload;
+ // Store accumulation result into a register
+ adder_out <= old_result + mult_reg;
+ end
+
+// Output accumulation result
+assign accum_out = adder_out;
+
+endmodule
+
+// Adapted variant of above
+module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) (
+ input clk,
+ input ce,
+ input rst,
+ input signed [SIZEIN-1:0] a, b,
+ output signed [SIZEOUT-1:0] accum_out,
+ output overflow
+);
+// Declare registers for intermediate values
+reg signed [SIZEIN-1:0] a_reg, b_reg, a_reg2, b_reg2;
+reg signed [2*SIZEIN-1:0] mult_reg = 0;
+reg signed [SIZEOUT:0] adder_out = 0;
+reg overflow_reg;
+always @(posedge clk) begin
+ //if (ce)
+ begin
+ a_reg <= a;
+ b_reg <= b;
+ a_reg2 <= a_reg;
+ b_reg2 <= b_reg;
+ mult_reg <= a_reg2 * b_reg2;
+ // Store accumulation result into a register
+ adder_out <= adder_out + mult_reg;
+ overflow_reg <= overflow;
+ end
+ if (rst) begin
+ a_reg <= 0;
+ a_reg2 <= 0;
+ b_reg <= 0;
+ b_reg2 <= 0;
+ mult_reg <= 0;
+ adder_out <= 0;
+ overflow_reg <= 1'b0;
+ end
+end
+assign overflow = (adder_out >= 2**(SIZEOUT-1)) | overflow_reg;
+
+// Output accumulation result
+assign accum_out = overflow ? 2**(SIZEOUT-1)-1 : adder_out;
+
+endmodule
diff --git a/tests/xilinx/macc.ys b/tests/xilinx/macc.ys
new file mode 100644
index 000000000..417a3b21b
--- /dev/null
+++ b/tests/xilinx/macc.ys
@@ -0,0 +1,31 @@
+read_verilog macc.v
+design -save read
+
+proc
+hierarchy -top macc
+#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd macc # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:FDRE
+select -assert-count 1 t:DSP48E1
+select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D
+
+design -load read
+proc
+hierarchy -top macc2
+#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd macc2 # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:DSP48E1
+select -assert-count 1 t:FDRE
+select -assert-count 1 t:LUT2
+select -assert-count 41 t:LUT3
+select -assert-none t:BUFG t:DSP48E1 t:FDRE t:LUT2 t:LUT3 %% t:* %D
diff --git a/tests/xilinx/macc_tb.v b/tests/xilinx/macc_tb.v
new file mode 100644
index 000000000..64aed05c4
--- /dev/null
+++ b/tests/xilinx/macc_tb.v
@@ -0,0 +1,96 @@
+`timescale 1ns / 1ps
+
+module testbench;
+
+ parameter SIZEIN = 16, SIZEOUT = 40;
+ reg clk, ce, rst;
+ reg signed [SIZEIN-1:0] a, b;
+ output signed [SIZEOUT-1:0] REF_accum_out, accum_out;
+ output REF_overflow, overflow;
+
+ integer errcount = 0;
+
+ reg ERROR_FLAG = 0;
+
+ task clkcycle;
+ begin
+ #5;
+ clk = ~clk;
+ #10;
+ clk = ~clk;
+ #2;
+ ERROR_FLAG = 0;
+ if (REF_accum_out !== accum_out) begin
+ $display("ERROR at %1t: REF_accum_out=%b UUT_accum_out=%b DIFF=%b", $time, REF_accum_out, accum_out, REF_accum_out ^ accum_out);
+ errcount = errcount + 1;
+ ERROR_FLAG = 1;
+ end
+ if (REF_overflow !== overflow) begin
+ $display("ERROR at %1t: REF_overflow=%b UUT_overflow=%b DIFF=%b", $time, REF_overflow, overflow, REF_overflow ^ overflow);
+ errcount = errcount + 1;
+ ERROR_FLAG = 1;
+ end
+ #3;
+ end
+ endtask
+
+ initial begin
+ //$dumpfile("test_macc.vcd");
+ //$dumpvars(0, testbench);
+
+ #2;
+ clk = 1'b0;
+ ce = 1'b0;
+ a = 0;
+ b = 0;
+
+ rst = 1'b1;
+ repeat (10) begin
+ #10;
+ clk = 1'b1;
+ #10;
+ clk = 1'b0;
+ #10;
+ clk = 1'b1;
+ #10;
+ clk = 1'b0;
+ end
+ rst = 1'b0;
+
+ repeat (10000) begin
+ clkcycle;
+ ce = 1; //$urandom & $urandom;
+ //rst = $urandom & $urandom & $urandom & $urandom & $urandom & $urandom;
+ a = $urandom & ~(1 << (SIZEIN-1));
+ b = $urandom & ~(1 << (SIZEIN-1));
+ end
+
+ if (errcount == 0) begin
+ $display("All tests passed.");
+ $finish;
+ end else begin
+ $display("Caught %1d errors.", errcount);
+ $stop;
+ end
+ end
+
+ macc2 ref (
+ .clk(clk),
+ .ce(ce),
+ .rst(rst),
+ .a(a),
+ .b(b),
+ .accum_out(REF_accum_out),
+ .overflow(REF_overflow)
+ );
+
+ macc2_uut uut (
+ .clk(clk),
+ .ce(ce),
+ .rst(rst),
+ .a(a),
+ .b(b),
+ .accum_out(accum_out),
+ .overflow(overflow)
+ );
+endmodule
diff --git a/tests/xilinx/mul_unsigned.v b/tests/xilinx/mul_unsigned.v
new file mode 100644
index 000000000..e3713a642
--- /dev/null
+++ b/tests/xilinx/mul_unsigned.v
@@ -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
diff --git a/tests/xilinx/mul_unsigned.ys b/tests/xilinx/mul_unsigned.ys
new file mode 100644
index 000000000..77990bd68
--- /dev/null
+++ b/tests/xilinx/mul_unsigned.ys
@@ -0,0 +1,10 @@
+read_verilog mul_unsigned.v
+proc
+hierarchy -top mul_unsigned
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:BUFG
+select -assert-count 1 t:DSP48E1
+select -assert-count 30 t:FDRE
+select -assert-none t:DSP48E1 t:FDRE t:BUFG %% t:* %D