Merge remote-tracking branch 'origin/master' into xaig_dff

22 files changed, 424 insertions, 0 deletions

diff --git a/tests/arch/ice40/.gitignore b/tests/arch/ice40/.gitignore
new file mode 100644
index 000000000..9a71dca69
--- /dev/null
+++ b/tests/arch/ice40/.gitignore
@@ -0,0 +1,4 @@
+*.log
+/run-test.mk
++*_synth.v
++*_testbench
diff --git a/tests/arch/ice40/add_sub.ys b/tests/arch/ice40/add_sub.ys
new file mode 100644
index 000000000..578ec0803
--- /dev/null
+++ b/tests/arch/ice40/add_sub.ys
@@ -0,0 +1,9 @@
+read_verilog ../common/add_sub.v
+hierarchy -top top
+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 11 t:SB_LUT4
+select -assert-count 6 t:SB_CARRY
+select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D
+
diff --git a/tests/arch/ice40/adffs.ys b/tests/arch/ice40/adffs.ys
new file mode 100644
index 000000000..e5dbabb43
--- /dev/null
+++ b/tests/arch/ice40/adffs.ys
@@ -0,0 +1,39 @@
+read_verilog ../common/adffs.v
+design -save read
+
+hierarchy -top adff
+proc
+equiv_opt -async2sync -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 adff # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_DFFR
+select -assert-none t:SB_DFFR %% t:* %D
+
+design -load read
+hierarchy -top adffn
+proc
+equiv_opt -async2sync -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 adffn # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_DFFR
+select -assert-count 1 t:SB_LUT4
+select -assert-none t:SB_DFFR t:SB_LUT4 %% t:* %D
+
+design -load read
+hierarchy -top dffs
+proc
+equiv_opt -async2sync -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 dffs # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_DFFSS
+select -assert-none t:SB_DFFSS %% t:* %D
+
+design -load read
+hierarchy -top ndffnr
+proc
+equiv_opt -async2sync -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 ndffnr # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_DFFNSR
+select -assert-count 1 t:SB_LUT4
+select -assert-none t:SB_DFFNSR t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/ice40/counter.ys b/tests/arch/ice40/counter.ys
new file mode 100644
index 000000000..f112eb97d
--- /dev/null
+++ b/tests/arch/ice40/counter.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/counter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -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 6 t:SB_CARRY
+select -assert-count 8 t:SB_DFFR
+select -assert-count 8 t:SB_LUT4
+select -assert-none t:SB_CARRY t:SB_DFFR t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/ice40/dffs.ys b/tests/arch/ice40/dffs.ys
new file mode 100644
index 000000000..b28a5a91f
--- /dev/null
+++ b/tests/arch/ice40/dffs.ys
@@ -0,0 +1,19 @@
+read_verilog ../common/dffs.v
+design -save read
+
+hierarchy -top dff
+proc
+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 dff # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_DFF
+select -assert-none t:SB_DFF %% t:* %D
+
+design -load read
+hierarchy -top dffe
+proc
+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 dffe # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_DFFE
+select -assert-none t:SB_DFFE %% t:* %D
\ No newline at end of file
diff --git a/tests/arch/ice40/dpram.v b/tests/arch/ice40/dpram.v
new file mode 100644
index 000000000..3ea4c1f27
--- /dev/null
+++ b/tests/arch/ice40/dpram.v
@@ -0,0 +1,23 @@
+/*
+Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 72].
+*/
+module top (din, write_en, waddr, wclk, raddr, rclk, dout);
+parameter addr_width = 8;
+parameter data_width = 8;
+input [addr_width-1:0] waddr, raddr;
+input [data_width-1:0] din;
+input write_en, wclk, rclk;
+output [data_width-1:0] dout;
+reg [data_width-1:0] dout;
+reg [data_width-1:0] mem [(1<<addr_width)-1:0]
+/* synthesis syn_ramstyle = "no_rw_check" */ ;
+always @(posedge wclk) // Write memory.
+begin
+if (write_en)
+mem[waddr] <= din; // Using write address bus.
+end
+always @(posedge rclk) // Read memory.
+begin
+dout <= mem[raddr]; // Using read address bus.
+end
+endmodule
diff --git a/tests/arch/ice40/dpram.ys b/tests/arch/ice40/dpram.ys
new file mode 100644
index 000000000..4f6a253ea
--- /dev/null
+++ b/tests/arch/ice40/dpram.ys
@@ -0,0 +1,15 @@
+read_verilog dpram.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+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 top
+select -assert-count 1 t:SB_RAM40_4K
+select -assert-none t:SB_RAM40_4K %% t:* %D
diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys
new file mode 100644
index 000000000..223ba070e
--- /dev/null
+++ b/tests/arch/ice40/fsm.ys
@@ -0,0 +1,16 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+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
+
+select -assert-count 4 t:SB_DFF
+select -assert-count 2 t:SB_DFFESR
+select -assert-count 15 t:SB_LUT4
+select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys
new file mode 100644
index 000000000..b17c69c91
--- /dev/null
+++ b/tests/arch/ice40/ice40_opt.ys
@@ -0,0 +1,26 @@
+read_verilog -icells -formal <<EOT
+module top(input CI, I0, output [1:0] CO, output O);
+    wire A = 1'b0, B = 1'b0;
+	\$__ICE40_CARRY_WRAPPER #(
+		//    A[0]: 1010 1010 1010 1010
+		//    A[1]: 1100 1100 1100 1100
+		//    A[2]: 1111 0000 1111 0000
+		//    A[3]: 1111 1111 0000 0000
+		.LUT(~16'b 0110_1001_1001_0110)
+	) u0 (
+		.A(A),
+		.B(B),
+		.CI(CI),
+		.I0(I0),
+		.I3(CI),
+		.CO(CO[0]),
+		.O(O)
+	);
+    SB_CARRY u1 (.I0(~A), .I1(~B), .CI(CI), .CO(CO[1]));
+endmodule
+EOT
+
+equiv_opt -assert -map +/ice40/cells_map.v -map +/ice40/cells_sim.v ice40_opt
+design -load postopt
+select -assert-count 1 t:*
+select -assert-count 1 t:$lut
diff --git a/tests/arch/ice40/latches.ys b/tests/arch/ice40/latches.ys
new file mode 100644
index 000000000..b06dd630b
--- /dev/null
+++ b/tests/arch/ice40/latches.ys
@@ -0,0 +1,33 @@
+read_verilog ../common/latches.v
+design -save read
+
+hierarchy -top latchp
+proc
+# Can't run any sort of equivalence check because latches are blown to LUTs
+synth_ice40
+cd latchp # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_LUT4
+
+select -assert-none t:SB_LUT4 %% t:* %D
+
+
+design -load read
+hierarchy -top latchn
+proc
+# Can't run any sort of equivalence check because latches are blown to LUTs
+synth_ice40
+cd latchn # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_LUT4
+
+select -assert-none t:SB_LUT4 %% t:* %D
+
+
+design -load read
+hierarchy -top latchsr
+proc
+# Can't run any sort of equivalence check because latches are blown to LUTs
+synth_ice40
+cd latchsr # Constrain all select calls below inside the top module
+select -assert-count 2 t:SB_LUT4
+
+select -assert-none t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/ice40/logic.ys b/tests/arch/ice40/logic.ys
new file mode 100644
index 000000000..7432f5b1f
--- /dev/null
+++ b/tests/arch/ice40/logic.ys
@@ -0,0 +1,7 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+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 9 t:SB_LUT4
+select -assert-none t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/ice40/macc.v b/tests/arch/ice40/macc.v
new file mode 100644
index 000000000..6f68e7500
--- /dev/null
+++ b/tests/arch/ice40/macc.v
@@ -0,0 +1,47 @@
+/*
+Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 77].
+*/
+module top(clk,a,b,c,set);
+parameter A_WIDTH = 6 /*4*/;
+parameter B_WIDTH = 6 /*3*/;
+input set;
+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 [(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;
+    end
+    else
+    begin
+        reg_tmp_c <= a * b + c;
+    end
+end
+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
+    if (!hold) begin
+        reg_a <= a;
+        reg_b <= b;
+        reg_tmp_c <= reg_a * reg_b + c;
+    end
+end
+endmodule
diff --git a/tests/arch/ice40/macc.ys b/tests/arch/ice40/macc.ys
new file mode 100644
index 000000000..fd30e79c5
--- /dev/null
+++ b/tests/arch/ice40/macc.ys
@@ -0,0 +1,25 @@
+read_verilog macc.v
+proc
+design -save read
+
+hierarchy -top top
+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 -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 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/arch/ice40/memory.ys b/tests/arch/ice40/memory.ys
new file mode 100644
index 000000000..c356e67fb
--- /dev/null
+++ b/tests/arch/ice40/memory.ys
@@ -0,0 +1,15 @@
+read_verilog ../common/memory.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd top
+select -assert-count 1 t:SB_RAM40_4K
+select -assert-none t:SB_RAM40_4K %% t:* %D
diff --git a/tests/arch/ice40/mul.ys b/tests/arch/ice40/mul.ys
new file mode 100644
index 000000000..9891b77d6
--- /dev/null
+++ b/tests/arch/ice40/mul.ys
@@ -0,0 +1,7 @@
+read_verilog ../common/mul.v
+hierarchy -top top
+equiv_opt -assert -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
diff --git a/tests/arch/ice40/mux.ys b/tests/arch/ice40/mux.ys
new file mode 100644
index 000000000..99822391d
--- /dev/null
+++ b/tests/arch/ice40/mux.ys
@@ -0,0 +1,40 @@
+read_verilog ../common/mux.v
+design -save read
+
+hierarchy -top mux2
+proc
+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 mux2 # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_LUT4
+select -assert-none t:SB_LUT4 %% t:* %D
+
+design -load read
+hierarchy -top mux4
+proc
+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 mux4 # Constrain all select calls below inside the top module
+select -assert-count 2 t:SB_LUT4
+
+select -assert-none t:SB_LUT4 %% t:* %D
+
+design -load read
+hierarchy -top mux8
+proc
+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 mux8 # Constrain all select calls below inside the top module
+select -assert-count 5 t:SB_LUT4
+
+select -assert-none t:SB_LUT4 %% t:* %D
+
+design -load read
+hierarchy -top mux16
+proc
+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 mux16 # Constrain all select calls below inside the top module
+select -assert-count 11 t:SB_LUT4
+
+select -assert-none t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/ice40/rom.v b/tests/arch/ice40/rom.v
new file mode 100644
index 000000000..0a0f41f37
--- /dev/null
+++ b/tests/arch/ice40/rom.v
@@ -0,0 +1,18 @@
+/*
+Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74].
+*/
+module top(data, addr);
+output [3:0] data;
+input [4:0] addr;
+always @(addr) begin
+case (addr)
+0 : data = 'h4;
+1 : data = 'h9;
+2 : data = 'h1;
+15 : data = 'h8;
+16 : data = 'h1;
+17 : data = 'h0;
+default : data = 'h0;
+endcase
+end
+endmodule
diff --git a/tests/arch/ice40/rom.ys b/tests/arch/ice40/rom.ys
new file mode 100644
index 000000000..41d214e2a
--- /dev/null
+++ b/tests/arch/ice40/rom.ys
@@ -0,0 +1,8 @@
+read_verilog rom.v
+proc
+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 5 t:SB_LUT4
+select -assert-none t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/ice40/run-test.sh b/tests/arch/ice40/run-test.sh
new file mode 100755
index 000000000..bf19b887d
--- /dev/null
+++ b/tests/arch/ice40/run-test.sh
@@ -0,0 +1,20 @@
+#!/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 -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
+		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
diff --git a/tests/arch/ice40/shifter.ys b/tests/arch/ice40/shifter.ys
new file mode 100644
index 000000000..08ea64f3d
--- /dev/null
+++ b/tests/arch/ice40/shifter.ys
@@ -0,0 +1,9 @@
+read_verilog ../common/shifter.v
+hierarchy -top top
+proc
+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 8 t:SB_DFF
+select -assert-none t:SB_DFF %% t:* %D
diff --git a/tests/arch/ice40/tribuf.ys b/tests/arch/ice40/tribuf.ys
new file mode 100644
index 000000000..10cded954
--- /dev/null
+++ b/tests/arch/ice40/tribuf.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+tribuf
+flatten
+synth
+equiv_opt -assert -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40 # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd tristate # Constrain all select calls below inside the top module
+select -assert-count 1 t:$_TBUF_
+select -assert-none t:$_TBUF_ %% t:* %D
diff --git a/tests/arch/ice40/wrapcarry.ys b/tests/arch/ice40/wrapcarry.ys
new file mode 100644
index 000000000..10c029e68
--- /dev/null
+++ b/tests/arch/ice40/wrapcarry.ys
@@ -0,0 +1,22 @@
+read_verilog <<EOT
+module top(input A, B, CI, output O, CO);
+	SB_CARRY carry (
+		.I0(A),
+		.I1(B),
+		.CI(CI),
+		.CO(CO)
+	);
+	SB_LUT4 #(
+		.LUT_INIT(16'b 0110_1001_1001_0110)
+	) adder (
+		.I0(1'b0),
+		.I1(A),
+		.I2(B),
+		.I3(1'b0),
+		.O(O)
+	);
+endmodule
+EOT
+
+ice40_wrapcarry
+select -assert-count 1 t:$__ICE40_CARRY_WRAPPER