103 files changed, 2257 insertions, 0 deletions
diff --git a/tests/arch/anlogic/.gitignore b/tests/arch/anlogic/.gitignore
new file mode 100644
index 000000000..9a71dca69
--- /dev/null
+++ b/tests/arch/anlogic/.gitignore
@@ -0,0 +1,4 @@
+*.log
+/run-test.mk
++*_synth.v
++*_testbench
diff --git a/tests/arch/anlogic/add_sub.ys b/tests/arch/anlogic/add_sub.ys
new file mode 100644
index 000000000..5396ce7ec
--- /dev/null
+++ b/tests/arch/anlogic/add_sub.ys
@@ -0,0 +1,10 @@
+read_verilog ../common/add_sub.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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 10 t:AL_MAP_ADDER
+select -assert-count 4 t:AL_MAP_LUT1
+
+select -assert-none t:AL_MAP_LUT1 t:AL_MAP_ADDER %% t:* %D
diff --git a/tests/arch/anlogic/counter.ys b/tests/arch/anlogic/counter.ys
new file mode 100644
index 000000000..d363ec24e
--- /dev/null
+++ b/tests/arch/anlogic/counter.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/counter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_ADDER
+select -assert-count 8 t:AL_MAP_SEQ
+select -assert-none t:AL_MAP_SEQ t:AL_MAP_ADDER %% t:* %D
diff --git a/tests/arch/anlogic/dffs.ys b/tests/arch/anlogic/dffs.ys
new file mode 100644
index 000000000..d3281ab89
--- /dev/null
+++ b/tests/arch/anlogic/dffs.ys
@@ -0,0 +1,20 @@
+read_verilog ../common/dffs.v
+design -save read
+
+hierarchy -top dff
+proc
+equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_SEQ
+select -assert-none t:AL_MAP_SEQ %% t:* %D
+
+design -load read
+hierarchy -top dffe
+proc
+equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_LUT3
+select -assert-count 1 t:AL_MAP_SEQ
+select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D
diff --git a/tests/arch/anlogic/fsm.ys b/tests/arch/anlogic/fsm.ys
new file mode 100644
index 000000000..0bcc4e011
--- /dev/null
+++ b/tests/arch/anlogic/fsm.ys
@@ -0,0 +1,18 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic
+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 1 t:AL_MAP_LUT2
+select -assert-count 5 t:AL_MAP_LUT5
+select -assert-count 1 t:AL_MAP_LUT6
+select -assert-count 6 t:AL_MAP_SEQ
+
+select -assert-none t:AL_MAP_LUT2 t:AL_MAP_LUT5 t:AL_MAP_LUT6 t:AL_MAP_SEQ %% t:* %D
diff --git a/tests/arch/anlogic/latches.ys b/tests/arch/anlogic/latches.ys
new file mode 100644
index 000000000..8d66f77b3
--- /dev/null
+++ b/tests/arch/anlogic/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_anlogic
+cd latchp # Constrain all select calls below inside the top module
+select -assert-count 1 t:AL_MAP_LUT3
+
+select -assert-none t:AL_MAP_LUT3 %% t:* %D
+
+
+design -load read
+hierarchy -top latchn
+proc
+# Can't run any sort of equivalence check because latches are blown to LUTs
+synth_anlogic
+cd latchn # Constrain all select calls below inside the top module
+select -assert-count 1 t:AL_MAP_LUT3
+
+select -assert-none t:AL_MAP_LUT3 %% t:* %D
+
+
+design -load read
+hierarchy -top latchsr
+proc
+# Can't run any sort of equivalence check because latches are blown to LUTs
+synth_anlogic
+cd latchsr # Constrain all select calls below inside the top module
+select -assert-count 1 t:AL_MAP_LUT5
+
+select -assert-none t:AL_MAP_LUT5 %% t:* %D
diff --git a/tests/arch/anlogic/logic.ys b/tests/arch/anlogic/logic.ys
new file mode 100644
index 000000000..125ee5d0f
--- /dev/null
+++ b/tests/arch/anlogic/logic.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_LUT1
+select -assert-count 6 t:AL_MAP_LUT2
+select -assert-count 2 t:AL_MAP_LUT4
+select -assert-none t:AL_MAP_LUT1 t:AL_MAP_LUT2 t:AL_MAP_LUT4 %% t:* %D
diff --git a/tests/arch/anlogic/memory.ys b/tests/arch/anlogic/memory.ys
new file mode 100644
index 000000000..87b93c2fe
--- /dev/null
+++ b/tests/arch/anlogic/memory.ys
@@ -0,0 +1,21 @@
+read_verilog ../common/memory.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#ERROR: Failed to import cell gate.mem.0.0.0 (type EG_LOGIC_DRAM16X4) to SAT database.
+#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd top
+
+select -assert-count 8  t:AL_MAP_LUT2
+select -assert-count 8  t:AL_MAP_LUT4
+select -assert-count 8   t:AL_MAP_LUT5
+select -assert-count 36 t:AL_MAP_SEQ
+select -assert-count 8  t:EG_LOGIC_DRAM16X4 #Why not AL_LOGIC_BRAM?
+select -assert-none t:AL_MAP_LUT2 t:AL_MAP_LUT4 t:AL_MAP_LUT5 t:AL_MAP_SEQ t:EG_LOGIC_DRAM16X4 %% t:* %D
diff --git a/tests/arch/anlogic/mux.ys b/tests/arch/anlogic/mux.ys
new file mode 100644
index 000000000..3d5fe7c9a
--- /dev/null
+++ b/tests/arch/anlogic/mux.ys
@@ -0,0 +1,42 @@
+read_verilog ../common/mux.v
+design -save read
+
+hierarchy -top mux2
+proc
+equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_LUT3
+
+select -assert-none t:AL_MAP_LUT3 %% t:* %D
+
+design -load read
+hierarchy -top mux4
+proc
+equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_LUT6
+
+select -assert-none t:AL_MAP_LUT6 %% t:* %D
+
+design -load read
+hierarchy -top mux8
+proc
+equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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 3 t:AL_MAP_LUT4
+select -assert-count 1 t:AL_MAP_LUT6
+
+select -assert-none t:AL_MAP_LUT4 t:AL_MAP_LUT6 %% t:* %D
+
+design -load read
+hierarchy -top mux16
+proc
+equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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 5 t:AL_MAP_LUT6
+
+select -assert-none t:AL_MAP_LUT6 %% t:* %D
diff --git a/tests/arch/anlogic/run-test.sh b/tests/arch/anlogic/run-test.sh
new file mode 100755
index 000000000..bf19b887d
--- /dev/null
+++ b/tests/arch/anlogic/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/anlogic/shifter.ys b/tests/arch/anlogic/shifter.ys
new file mode 100644
index 000000000..12df44b2a
--- /dev/null
+++ b/tests/arch/anlogic/shifter.ys
@@ -0,0 +1,10 @@
+read_verilog ../common/shifter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_SEQ
+
+select -assert-none t:AL_MAP_SEQ %% t:* %D
diff --git a/tests/arch/anlogic/tribuf.ys b/tests/arch/anlogic/tribuf.ys
new file mode 100644
index 000000000..eaa073750
--- /dev/null
+++ b/tests/arch/anlogic/tribuf.ys
@@ -0,0 +1,9 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+flatten
+equiv_opt -assert -map +/anlogic/cells_sim.v -map +/simcells.v synth_anlogic # 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/common/add_sub.v b/tests/arch/common/add_sub.v
new file mode 100644
index 000000000..77e5f5745
--- /dev/null
+++ b/tests/arch/common/add_sub.v
@@ -0,0 +1,12 @@
+module top
+(
+    input [3:0] x,
+    input [3:0] y,
+
+    output [3:0] A,
+    output [3:0] B
+);
+
+    assign A =  x + y;
+    assign B =  x - y;
+endmodule
diff --git a/tests/arch/common/adffs.v b/tests/arch/common/adffs.v
new file mode 100644
index 000000000..576bd81a6
--- /dev/null
+++ b/tests/arch/common/adffs.v
@@ -0,0 +1,43 @@
+module adff( input d, clk, clr, output reg q );
+    initial begin
+        q = 0;
+    end
+	  always @( posedge clk, posedge clr )
+      if ( clr )
+        q <= 1'b0;
+      else
+        q <= d;
+endmodule
+
+module adffn( input d, clk, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+	  always @( posedge clk, negedge clr )
+		  if ( !clr )
+			  q <= 1'b0;
+  		else
+        q <= d;
+endmodule
+
+module dffs( input d, clk, pre, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+    always @( posedge clk )
+      if ( pre )
+        q <= 1'b1;
+      else
+        q <= d;
+endmodule
+
+module ndffnr( input d, clk, pre, clr, output reg q );
+    initial begin
+      q = 0;
+    end
+    always @( negedge clk )
+      if ( !clr )
+        q <= 1'b0;
+      else
+        q <= d;
+endmodule
diff --git a/tests/arch/common/counter.v b/tests/arch/common/counter.v
new file mode 100644
index 000000000..9746fd701
--- /dev/null
+++ b/tests/arch/common/counter.v
@@ -0,0 +1,11 @@
+module top ( out, clk, reset );
+    output [7:0] out;
+    input clk, reset;
+    reg [7:0] out;
+
+    always @(posedge clk, posedge reset)
+      if (reset)
+          out <= 8'b0;
+      else
+          out <= out + 1;
+endmodule
diff --git a/tests/arch/common/dffs.v b/tests/arch/common/dffs.v
new file mode 100644
index 000000000..636252d16
--- /dev/null
+++ b/tests/arch/common/dffs.v
@@ -0,0 +1,13 @@
+module dff ( input d, clk, output reg q );
+	  always @( posedge clk )
+        q <= d;
+endmodule
+
+module dffe( input d, clk, en, output reg q );
+    initial begin
+        q = 0;
+    end
+	  always @( posedge clk )
+        if ( en )
+              q <= d;
+endmodule
diff --git a/tests/arch/common/fsm.v b/tests/arch/common/fsm.v
new file mode 100644
index 000000000..9d3fbb64a
--- /dev/null
+++ b/tests/arch/common/fsm.v
@@ -0,0 +1,51 @@
+ module fsm ( clock, reset, req_0, req_1, gnt_0, gnt_1 );
+    input   clock,reset,req_0,req_1;
+    output  gnt_0,gnt_1;
+    wire    clock,reset,req_0,req_1;
+    reg     gnt_0,gnt_1;
+
+    parameter SIZE = 3;
+    parameter IDLE = 3'b001;
+    parameter GNT0 = 3'b010;
+    parameter GNT1 = 3'b100;
+    parameter GNT2 = 3'b101;
+
+    reg [SIZE-1:0] state;
+    reg [SIZE-1:0] next_state;
+
+    always @ (posedge clock)
+        begin : FSM
+          if (reset == 1'b1) begin
+            state <=  #1  IDLE;
+            gnt_0 <= 0;
+            gnt_1 <= 0;
+          end 
+          else
+            case(state)
+              IDLE :  if (req_0 == 1'b1) begin
+                          state <=  #1  GNT0;
+                          gnt_0 <= 1;
+                      end else if (req_1 == 1'b1) begin
+                          gnt_1 <= 1;
+                          state <=  #1  GNT0;
+                      end else begin
+                          state <=  #1  IDLE;
+                      end
+              GNT0 :  if (req_0 == 1'b1) begin
+                          state <=  #1  GNT0;
+                      end else begin
+                          gnt_0 <= 0;
+                          state <=  #1  IDLE;
+                      end
+              GNT1 :  if (req_1 == 1'b1) begin
+                          state <=  #1  GNT2;
+                          gnt_1 <= req_0;
+                      end
+              GNT2 :  if (req_0 == 1'b1) begin
+                          state <=  #1  GNT1;
+                          gnt_1 <= req_1;
+                      end
+              default : state <=  #1  IDLE;
+            endcase
+        end
+endmodule
diff --git a/tests/arch/common/latches.v b/tests/arch/common/latches.v
new file mode 100644
index 000000000..60b757103
--- /dev/null
+++ b/tests/arch/common/latches.v
@@ -0,0 +1,21 @@
+module latchp ( input d, clk, en, output reg q );
+	always @*
+		if ( en )
+			q <= d;
+endmodule
+
+module latchn ( input d, clk, en, output reg q );
+	always @*
+		if ( !en )
+			q <= d;
+endmodule
+
+module latchsr ( input d, clk, en, clr, pre, output reg q );
+	always @*
+		if ( clr )
+			q <= 1'b0;
+		else if ( pre )
+			q <= 1'b1;
+		else if ( en )
+			q <= d;
+endmodule
diff --git a/tests/arch/common/logic.v b/tests/arch/common/logic.v
new file mode 100644
index 000000000..c17899fa0
--- /dev/null
+++ b/tests/arch/common/logic.v
@@ -0,0 +1,16 @@
+module top
+(
+    input [0:7] in,
+    output B1,B2,B3,B4,B5,B6,B7,B8,B9,B10
+);
+    assign B1 =  in[0] & in[1];
+    assign B2 =  in[0] | in[1];
+    assign B3 =  in[0] ~& in[1];
+    assign B4 =  in[0] ~| in[1];
+    assign B5 =  in[0] ^ in[1];
+    assign B6 =  in[0] ~^ in[1];
+    assign B7 =  ~in[0];
+    assign B8 =  in[0];
+    assign B9 =  in[0:1] && in [2:3];
+    assign B10 =  in[0:1] || in [2:3];
+endmodule
diff --git a/tests/arch/common/memory.v b/tests/arch/common/memory.v
new file mode 100644
index 000000000..cb7753f7b
--- /dev/null
+++ b/tests/arch/common/memory.v
@@ -0,0 +1,21 @@
+module top
+(
+	input [7:0] data_a,
+	input [6:1] addr_a,
+	input we_a, clk,
+	output reg [7:0] q_a
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+
+	// Port A
+	always @ (posedge clk)
+	begin
+		if (we_a)
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+		q_a <= ram[addr_a];
+	end
+endmodule
diff --git a/tests/arch/common/mul.v b/tests/arch/common/mul.v
new file mode 100644
index 000000000..437a91cfc
--- /dev/null
+++ b/tests/arch/common/mul.v
@@ -0,0 +1,9 @@
+module top
+(
+    input [5:0] x,
+    input [5:0] y,
+
+    output [11:0] A,
+);
+    assign A =  x * y;
+endmodule
diff --git a/tests/arch/common/mux.v b/tests/arch/common/mux.v
new file mode 100644
index 000000000..71c1ac7f2
--- /dev/null
+++ b/tests/arch/common/mux.v
@@ -0,0 +1,60 @@
+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+
+    always @(*)
+		Y = (S)? B : A;
+endmodule
+
+module mux4 ( S, D, Y );
+    input[1:0] S;
+    input[3:0] D;
+    output Y;
+
+    reg Y;
+    wire[1:0] S;
+    wire[3:0] D;
+
+    always @*
+    begin
+        case( S )
+            0 : Y = D[0];
+            1 : Y = D[1];
+            2 : Y = D[2];
+            3 : Y = D[3];
+        endcase
+    end
+endmodule
+
+module mux8 ( S, D, Y );
+    input[2:0] S;
+    input[7:0] D;
+    output Y;
+
+    reg Y;
+    wire[2:0] S;
+    wire[7:0] D;
+
+    always @*
+    begin
+        case( S )
+            0 : Y = D[0];
+            1 : Y = D[1];
+            2 : Y = D[2];
+            3 : Y = D[3];
+            4 : Y = D[4];
+            5 : Y = D[5];
+            6 : Y = D[6];
+            7 : Y = D[7];
+        endcase
+    end
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+    assign Y = D[S];
+endmodule
diff --git a/tests/arch/common/shifter.v b/tests/arch/common/shifter.v
new file mode 100644
index 000000000..cace3b588
--- /dev/null
+++ b/tests/arch/common/shifter.v
@@ -0,0 +1,11 @@
+module top(out, clk, in);
+    output [7:0] out;
+    input signed clk, in;
+    reg signed [7:0] out = 0;
+
+    always @(posedge clk)
+	begin
+		out    <= out >> 1;
+		out[7] <= in;
+	end    
+endmodule
diff --git a/tests/arch/common/tribuf.v b/tests/arch/common/tribuf.v
new file mode 100644
index 000000000..e1d701611
--- /dev/null
+++ b/tests/arch/common/tribuf.v
@@ -0,0 +1,8 @@
+module tristate(en, i, o);
+    input en;
+    input i;
+    output reg o;
+
+    always @(en or i)
+        o <= (en)? i : 1'bZ;
+endmodule
diff --git a/tests/arch/ecp5/.gitignore b/tests/arch/ecp5/.gitignore
new file mode 100644
index 000000000..1d329c933
--- /dev/null
+++ b/tests/arch/ecp5/.gitignore
@@ -0,0 +1,2 @@
+*.log
+/run-test.mk
diff --git a/tests/arch/ecp5/add_sub.ys b/tests/arch/ecp5/add_sub.ys
new file mode 100644
index 000000000..d85ce792e
--- /dev/null
+++ b/tests/arch/ecp5/add_sub.ys
@@ -0,0 +1,9 @@
+read_verilog ../common/add_sub.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 10 t:LUT4
+select -assert-none t:LUT4 %% t:* %D
+
diff --git a/tests/arch/ecp5/adffs.ys b/tests/arch/ecp5/adffs.ys
new file mode 100644
index 000000000..01605df70
--- /dev/null
+++ b/tests/arch/ecp5/adffs.ys
@@ -0,0 +1,40 @@
+read_verilog ../common/adffs.v
+design -save read
+
+hierarchy -top adff
+proc
+equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF
+select -assert-none t:TRELLIS_FF %% t:* %D
+
+design -load read
+hierarchy -top adffn
+proc
+equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF
+select -assert-count 1 t:LUT4
+select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D
+
+design -load read
+hierarchy -top dffs
+proc
+equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF
+select -assert-count 1 t:LUT4
+select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D
+
+design -load read
+hierarchy -top ndffnr
+proc
+equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF
+select -assert-count 1 t:LUT4
+select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D
diff --git a/tests/arch/ecp5/counter.ys b/tests/arch/ecp5/counter.ys
new file mode 100644
index 000000000..f9f60fbff
--- /dev/null
+++ b/tests/arch/ecp5/counter.ys
@@ -0,0 +1,10 @@
+read_verilog ../common/counter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # 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 4 t:CCU2C
+select -assert-count 8 t:TRELLIS_FF
+select -assert-none t:CCU2C t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/ecp5/dffs.ys b/tests/arch/ecp5/dffs.ys
new file mode 100644
index 000000000..be97972db
--- /dev/null
+++ b/tests/arch/ecp5/dffs.ys
@@ -0,0 +1,19 @@
+read_verilog ../common/dffs.v
+design -save read
+
+hierarchy -top dff
+proc
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF
+select -assert-none t:TRELLIS_FF %% t:* %D
+
+design -load read
+hierarchy -top dffe
+proc
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF
+select -assert-none t:TRELLIS_FF %% t:* %D
+\ No newline at end of file
diff --git a/tests/arch/ecp5/dpram.v b/tests/arch/ecp5/dpram.v
new file mode 100644
index 000000000..3ea4c1f27
--- /dev/null
+++ b/tests/arch/ecp5/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/ecp5/dpram.ys b/tests/arch/ecp5/dpram.ys
new file mode 100644
index 000000000..3bc6bc1d0
--- /dev/null
+++ b/tests/arch/ecp5/dpram.ys
@@ -0,0 +1,18 @@
+read_verilog dpram.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+
+#Blocked by issue #1358 (Missing ECP5 simulation models)
+#ERROR: Failed to import cell gate.mem.0.0.0 (type DP16KD) to SAT database.
+#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd top
+select -assert-count 1 t:DP16KD
+select -assert-none t:DP16KD %% t:* %D
diff --git a/tests/arch/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys
new file mode 100644
index 000000000..ba91e5fc0
--- /dev/null
+++ b/tests/arch/ecp5/fsm.ys
@@ -0,0 +1,17 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+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 1 t:L6MUX21
+select -assert-count 15 t:LUT4
+select -assert-count 6 t:PFUMX
+select -assert-count 6 t:TRELLIS_FF
+select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/ecp5/latches.ys b/tests/arch/ecp5/latches.ys
new file mode 100644
index 000000000..3d011d74f
--- /dev/null
+++ b/tests/arch/ecp5/latches.ys
@@ -0,0 +1,34 @@
+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_ecp5
+cd latchp # Constrain all select calls below inside the top module
+select -assert-count 1 t:LUT4
+
+select -assert-none t: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_ecp5
+cd latchn # Constrain all select calls below inside the top module
+select -assert-count 1 t:LUT4
+
+select -assert-none t: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_ecp5
+cd latchsr # Constrain all select calls below inside the top module
+select -assert-count 2 t:LUT4
+select -assert-count 1 t:PFUMX
+
+select -assert-none t:LUT4 t:PFUMX %% t:* %D
diff --git a/tests/arch/ecp5/logic.ys b/tests/arch/ecp5/logic.ys
new file mode 100644
index 000000000..3298b198f
--- /dev/null
+++ b/tests/arch/ecp5/logic.ys
@@ -0,0 +1,8 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:LUT4
+select -assert-none t:LUT4 %% t:* %D
diff --git a/tests/arch/ecp5/macc.v b/tests/arch/ecp5/macc.v
new file mode 100644
index 000000000..63a3d3a74
--- /dev/null
+++ b/tests/arch/ecp5/macc.v
@@ -0,0 +1,25 @@
+/*
+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 = 4;
+parameter B_WIDTH = 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
diff --git a/tests/arch/ecp5/macc.ys b/tests/arch/ecp5/macc.ys
new file mode 100644
index 000000000..1863ea4d2
--- /dev/null
+++ b/tests/arch/ecp5/macc.ys
@@ -0,0 +1,13 @@
+read_verilog macc.v
+hierarchy -top top
+proc
+# Blocked by issue #1358 (Missing ECP5 simulation models)
+#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
+equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # 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:MULT18X18D
+select -assert-count 4 t:CCU2C
+select -assert-count 7 t:TRELLIS_FF
+
+select -assert-none t:CCU2C t:MULT18X18D t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/ecp5/memory.ys b/tests/arch/ecp5/memory.ys
new file mode 100644
index 000000000..c82b7b405
--- /dev/null
+++ b/tests/arch/ecp5/memory.ys
@@ -0,0 +1,19 @@
+read_verilog ../common/memory.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+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 24 t:L6MUX21
+select -assert-count 71 t:LUT4
+select -assert-count 32 t:PFUMX
+select -assert-count 8 t:TRELLIS_DPR16X4
+select -assert-count 35 t:TRELLIS_FF
+select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_DPR16X4 t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/ecp5/mul.ys b/tests/arch/ecp5/mul.ys
new file mode 100644
index 000000000..2105be52c
--- /dev/null
+++ b/tests/arch/ecp5/mul.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/mul.v
+hierarchy -top top
+proc
+# Blocked by issue #1358 (Missing ECP5 simulation models)
+#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
+equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # 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:MULT18X18D
+select -assert-none t:MULT18X18D %% t:* %D
diff --git a/tests/arch/ecp5/mux.ys b/tests/arch/ecp5/mux.ys
new file mode 100644
index 000000000..92463aa32
--- /dev/null
+++ b/tests/arch/ecp5/mux.ys
@@ -0,0 +1,46 @@
+read_verilog ../common/mux.v
+design -save read
+
+hierarchy -top mux2
+proc
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:LUT4
+select -assert-none t:LUT4 %% t:* %D
+
+design -load read
+hierarchy -top mux4
+proc
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:L6MUX21
+select -assert-count 4 t:LUT4
+select -assert-count 2 t:PFUMX
+
+select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D
+
+design -load read
+hierarchy -top mux8
+proc
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:L6MUX21
+select -assert-count 7 t:LUT4
+select -assert-count 2 t:PFUMX
+
+select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D
+
+design -load read
+hierarchy -top mux16
+proc
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 8 t:L6MUX21
+select -assert-count 26 t:LUT4
+select -assert-count 12 t:PFUMX
+
+select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D
diff --git a/tests/arch/ecp5/rom.v b/tests/arch/ecp5/rom.v
new file mode 100644
index 000000000..0a0f41f37
--- /dev/null
+++ b/tests/arch/ecp5/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/ecp5/rom.ys b/tests/arch/ecp5/rom.ys
new file mode 100644
index 000000000..98645ae43
--- /dev/null
+++ b/tests/arch/ecp5/rom.ys
@@ -0,0 +1,10 @@
+read_verilog rom.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:LUT4
+select -assert-count 3 t:PFUMX
+select -assert-none t:LUT4 t:PFUMX %% t:* %D
diff --git a/tests/arch/ecp5/run-test.sh b/tests/arch/ecp5/run-test.sh
new file mode 100755
index 000000000..bf19b887d
--- /dev/null
+++ b/tests/arch/ecp5/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/ecp5/shifter.ys b/tests/arch/ecp5/shifter.ys
new file mode 100644
index 000000000..3f0079f4a
--- /dev/null
+++ b/tests/arch/ecp5/shifter.ys
@@ -0,0 +1,10 @@
+read_verilog ../common/shifter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF
+select -assert-none t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/ecp5/tribuf.ys b/tests/arch/ecp5/tribuf.ys
new file mode 100644
index 000000000..0118705a2
--- /dev/null
+++ b/tests/arch/ecp5/tribuf.ys
@@ -0,0 +1,9 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+flatten
+equiv_opt -assert -map +/ecp5/cells_sim.v -map +/simcells.v synth_ecp5 # 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/efinix/.gitignore b/tests/arch/efinix/.gitignore
new file mode 100644
index 000000000..b48f808a1
--- /dev/null
+++ b/tests/arch/efinix/.gitignore
@@ -0,0 +1,3 @@
+/*.log
+/*.out
+/run-test.mk
diff --git a/tests/arch/efinix/add_sub.ys b/tests/arch/efinix/add_sub.ys
new file mode 100644
index 000000000..20523c059
--- /dev/null
+++ b/tests/arch/efinix/add_sub.ys
@@ -0,0 +1,10 @@
+read_verilog ../common/add_sub.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 10 t:EFX_ADD
+select -assert-count 4  t:EFX_LUT4
+select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D
+
diff --git a/tests/arch/efinix/adffs.ys b/tests/arch/efinix/adffs.ys
new file mode 100644
index 000000000..49dc7f256
--- /dev/null
+++ b/tests/arch/efinix/adffs.ys
@@ -0,0 +1,50 @@
+read_verilog ../common/adffs.v
+design -save read
+
+hierarchy -top adff
+proc
+equiv_opt -async2sync -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF
+select -assert-count 1 t:EFX_GBUFCE
+
+select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
+
+
+design -load read
+hierarchy -top adffn
+proc
+equiv_opt -async2sync -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF
+select -assert-count 1 t:EFX_GBUFCE
+
+select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
+
+
+design -load read
+hierarchy -top dffs
+proc
+equiv_opt -async2sync -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF
+select -assert-count 1 t:EFX_GBUFCE
+select -assert-count 1 t:EFX_LUT4
+
+select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
+
+
+design -load read
+hierarchy -top ndffnr
+proc
+equiv_opt -async2sync -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF
+select -assert-count 1 t:EFX_GBUFCE
+select -assert-count 1 t:EFX_LUT4
+
+select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
diff --git a/tests/arch/efinix/counter.ys b/tests/arch/efinix/counter.ys
new file mode 100644
index 000000000..d20b8ae27
--- /dev/null
+++ b/tests/arch/efinix/counter.ys
@@ -0,0 +1,12 @@
+read_verilog ../common/counter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -map +/efinix/cells_sim.v synth_efinix # 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:EFX_GBUFCE
+select -assert-count 8 t:EFX_FF
+select -assert-count 9 t:EFX_ADD
+select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_ADD %% t:* %D
diff --git a/tests/arch/efinix/dffs.ys b/tests/arch/efinix/dffs.ys
new file mode 100644
index 000000000..af787ab67
--- /dev/null
+++ b/tests/arch/efinix/dffs.ys
@@ -0,0 +1,24 @@
+read_verilog ../common/dffs.v
+design -save read
+
+hierarchy -top dff
+proc
+equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF
+select -assert-count 1 t:EFX_GBUFCE
+
+select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
+
+design -load read
+hierarchy -top dffe
+proc
+equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF
+select -assert-count 1 t:EFX_GBUFCE
+select -assert-count 1 t:EFX_LUT4
+
+select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
diff --git a/tests/arch/efinix/fsm.ys b/tests/arch/efinix/fsm.ys
new file mode 100644
index 000000000..a2db2ad98
--- /dev/null
+++ b/tests/arch/efinix/fsm.ys
@@ -0,0 +1,16 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix
+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 1  t:EFX_GBUFCE
+select -assert-count 6  t:EFX_FF
+select -assert-count 15 t:EFX_LUT4
+select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D
diff --git a/tests/arch/efinix/latches.ys b/tests/arch/efinix/latches.ys
new file mode 100644
index 000000000..1b1c00023
--- /dev/null
+++ b/tests/arch/efinix/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_efinix
+cd latchp # Constrain all select calls below inside the top module
+select -assert-count 1 t:EFX_LUT4
+
+select -assert-none t:EFX_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_efinix
+cd latchn # Constrain all select calls below inside the top module
+select -assert-count 1 t:EFX_LUT4
+
+select -assert-none t:EFX_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_efinix
+cd latchsr # Constrain all select calls below inside the top module
+select -assert-count 2 t:EFX_LUT4
+
+select -assert-none t:EFX_LUT4 %% t:* %D
diff --git a/tests/arch/efinix/logic.ys b/tests/arch/efinix/logic.ys
new file mode 100644
index 000000000..76e98e079
--- /dev/null
+++ b/tests/arch/efinix/logic.ys
@@ -0,0 +1,9 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_LUT4
+select -assert-none t:EFX_LUT4 %% t:* %D
diff --git a/tests/arch/efinix/memory.ys b/tests/arch/efinix/memory.ys
new file mode 100644
index 000000000..6f6acdcde
--- /dev/null
+++ b/tests/arch/efinix/memory.ys
@@ -0,0 +1,18 @@
+read_verilog ../common/memory.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#ERROR: Called with -verify and proof did fail!
+#sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
+sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd top
+select -assert-count 1 t:EFX_GBUFCE
+select -assert-count 1 t:EFX_RAM_5K
+select -assert-none t:EFX_GBUFCE t:EFX_RAM_5K %% t:* %D
diff --git a/tests/arch/efinix/mux.ys b/tests/arch/efinix/mux.ys
new file mode 100644
index 000000000..b46f641e1
--- /dev/null
+++ b/tests/arch/efinix/mux.ys
@@ -0,0 +1,41 @@
+read_verilog ../common/mux.v
+design -save read
+
+hierarchy -top mux2
+proc
+equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_LUT4
+
+select -assert-none t:EFX_LUT4 %% t:* %D
+
+design -load read
+hierarchy -top mux4
+proc
+equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_LUT4
+
+select -assert-none t:EFX_LUT4 %% t:* %D
+
+design -load read
+hierarchy -top mux8
+proc
+equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_LUT4
+
+select -assert-none t:EFX_LUT4 %% t:* %D
+
+design -load read
+hierarchy -top mux16
+proc
+equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 12 t:EFX_LUT4
+
+select -assert-none t:EFX_LUT4 %% t:* %D
diff --git a/tests/arch/efinix/run-test.sh b/tests/arch/efinix/run-test.sh
new file mode 100755
index 000000000..bf19b887d
--- /dev/null
+++ b/tests/arch/efinix/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/efinix/shifter.ys b/tests/arch/efinix/shifter.ys
new file mode 100644
index 000000000..54f71167f
--- /dev/null
+++ b/tests/arch/efinix/shifter.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/shifter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_GBUFCE
+select -assert-count 8  t:EFX_FF
+select -assert-none t:EFX_GBUFCE t:EFX_FF %% t:* %D
diff --git a/tests/arch/efinix/tribuf.ys b/tests/arch/efinix/tribuf.ys
new file mode 100644
index 000000000..47904f2d5
--- /dev/null
+++ b/tests/arch/efinix/tribuf.ys
@@ -0,0 +1,12 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+tribuf
+flatten
+synth
+equiv_opt -assert -map +/efinix/cells_sim.v -map +/simcells.v synth_efinix # 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
+#Internal cell type used. Need support it.
+select -assert-count 1 t:$_TBUF_
+select -assert-none t:$_TBUF_ %% t:* %D
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
diff --git a/tests/arch/xilinx/.gitignore b/tests/arch/xilinx/.gitignore
new file mode 100644
index 000000000..c99b79371
--- /dev/null
+++ b/tests/arch/xilinx/.gitignore
@@ -0,0 +1,5 @@
+/*.log
+/*.out
+/run-test.mk
+/*_uut.v
+/test_macc
diff --git a/tests/arch/xilinx/add_sub.ys b/tests/arch/xilinx/add_sub.ys
new file mode 100644
index 000000000..9dbddce47
--- /dev/null
+++ b/tests/arch/xilinx/add_sub.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/add_sub.v
+hierarchy -top top
+proc
+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 top # Constrain all select calls below inside the top module
+select -assert-count 14 t:LUT2
+select -assert-count 6 t:MUXCY
+select -assert-count 8 t:XORCY
+select -assert-none t:LUT2 t:MUXCY t:XORCY %% t:* %D
+
diff --git a/tests/arch/xilinx/adffs.ys b/tests/arch/xilinx/adffs.ys
new file mode 100644
index 000000000..12c34415e
--- /dev/null
+++ b/tests/arch/xilinx/adffs.ys
@@ -0,0 +1,51 @@
+read_verilog ../common/adffs.v
+design -save read
+
+hierarchy -top adff
+proc
+equiv_opt -async2sync  -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 adff # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:FDCE
+
+select -assert-none t:BUFG t:FDCE %% t:* %D
+
+
+design -load read
+hierarchy -top adffn
+proc
+equiv_opt -async2sync  -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 adffn # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:FDCE
+select -assert-count 1 t:LUT1
+
+select -assert-none t:BUFG t:FDCE t:LUT1 %% t:* %D
+
+
+design -load read
+hierarchy -top dffs
+proc
+equiv_opt -async2sync  -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 dffs # 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:LUT2
+
+select -assert-none t:BUFG t:FDRE t:LUT2 %% t:* %D
+
+
+design -load read
+hierarchy -top ndffnr
+proc
+equiv_opt -async2sync  -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 ndffnr # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:FDRE_1
+select -assert-count 1 t:LUT2
+
+select -assert-none t:BUFG t:FDRE_1 t:LUT2 %% t:* %D
diff --git a/tests/arch/xilinx/counter.ys b/tests/arch/xilinx/counter.ys
new file mode 100644
index 000000000..57b645d19
--- /dev/null
+++ b/tests/arch/xilinx/counter.ys
@@ -0,0 +1,14 @@
+read_verilog ../common/counter.v
+hierarchy -top top
+proc
+flatten
+equiv_opt -async2sync -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 top # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:BUFG
+select -assert-count 8 t:FDCE
+select -assert-count 1 t:LUT1
+select -assert-count 7 t:MUXCY
+select -assert-count 8 t:XORCY
+select -assert-none t:BUFG t:FDCE t:LUT1 t:MUXCY t:XORCY %% t:* %D
diff --git a/tests/arch/xilinx/dffs.ys b/tests/arch/xilinx/dffs.ys
new file mode 100644
index 000000000..0bba4858f
--- /dev/null
+++ b/tests/arch/xilinx/dffs.ys
@@ -0,0 +1,25 @@
+read_verilog ../common/dffs.v
+design -save read
+
+hierarchy -top dff
+proc
+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 dff # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:FDRE
+
+select -assert-none t:BUFG t:FDRE %% t:* %D
+
+
+design -load read
+hierarchy -top dffe
+proc
+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 dffe # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:FDRE
+
+select -assert-none t:BUFG t:FDRE %% t:* %D
+
diff --git a/tests/arch/xilinx/dsp_simd.ys b/tests/arch/xilinx/dsp_simd.ys
new file mode 100644
index 000000000..956952327
--- /dev/null
+++ b/tests/arch/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/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys
new file mode 100644
index 000000000..2a72c34e8
--- /dev/null
+++ b/tests/arch/xilinx/fsm.ys
@@ -0,0 +1,18 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+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 1 t:BUFG
+select -assert-count 5 t:FDRE
+select -assert-count 1 t:LUT3
+select -assert-count 2 t:LUT4
+select -assert-count 4 t:LUT6
+select -assert-none t:BUFG t:FDRE t:LUT3 t:LUT4 t:LUT6 %% t:* %D
diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys
new file mode 100644
index 000000000..fe7887e8d
--- /dev/null
+++ b/tests/arch/xilinx/latches.ys
@@ -0,0 +1,35 @@
+read_verilog ../common/latches.v
+design -save read
+
+hierarchy -top latchp
+proc
+equiv_opt -async2sync -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 latchp # Constrain all select calls below inside the top module
+select -assert-count 1 t:LDCE
+
+select -assert-none t:LDCE %% t:* %D
+
+
+design -load read
+hierarchy -top latchn
+proc
+equiv_opt -async2sync -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 latchn # Constrain all select calls below inside the top module
+select -assert-count 1 t:LDCE
+select -assert-count 1 t:LUT1
+
+select -assert-none t:LDCE t:LUT1 %% t:* %D
+
+
+design -load read
+hierarchy -top latchsr
+proc
+equiv_opt -async2sync -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 latchsr # Constrain all select calls below inside the top module
+select -assert-count 1 t:LDCE
+select -assert-count 2 t:LUT3
+
+select -assert-none t:LDCE t:LUT3 %% t:* %D
diff --git a/tests/arch/xilinx/logic.ys b/tests/arch/xilinx/logic.ys
new file mode 100644
index 000000000..c0f6da302
--- /dev/null
+++ b/tests/arch/xilinx/logic.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+proc
+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 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
diff --git a/tests/arch/xilinx/macc.sh b/tests/arch/xilinx/macc.sh
new file mode 100644
index 000000000..2272679ee
--- /dev/null
+++ b/tests/arch/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/arch/xilinx/macc.v b/tests/arch/xilinx/macc.v
new file mode 100644
index 000000000..e36b2bab1
--- /dev/null
+++ b/tests/arch/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/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys
new file mode 100644
index 000000000..6e884b35a
--- /dev/null
+++ b/tests/arch/xilinx/macc.ys
@@ -0,0 +1,31 @@
+read_verilog macc.v
+design -save read
+
+hierarchy -top macc
+proc
+#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
+hierarchy -top macc2
+proc
+#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/arch/xilinx/macc_tb.v b/tests/arch/xilinx/macc_tb.v
new file mode 100644
index 000000000..64aed05c4
--- /dev/null
+++ b/tests/arch/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/arch/xilinx/memory.ys b/tests/arch/xilinx/memory.ys
new file mode 100644
index 000000000..da1ed0e49
--- /dev/null
+++ b/tests/arch/xilinx/memory.ys
@@ -0,0 +1,17 @@
+read_verilog ../common/memory.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+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:BUFG
+select -assert-count 8 t:FDRE
+select -assert-count 8 t:RAM64X1D
+select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D
diff --git a/tests/arch/xilinx/mul.ys b/tests/arch/xilinx/mul.ys
new file mode 100644
index 000000000..d76814966
--- /dev/null
+++ b/tests/arch/xilinx/mul.ys
@@ -0,0 +1,9 @@
+read_verilog ../common/mul.v
+hierarchy -top top
+proc
+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 top # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:DSP48E1
+select -assert-none t:DSP48E1 %% t:* %D
diff --git a/tests/arch/xilinx/mul_unsigned.v b/tests/arch/xilinx/mul_unsigned.v
new file mode 100644
index 000000000..e3713a642
--- /dev/null
+++ b/tests/arch/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/arch/xilinx/mul_unsigned.ys b/tests/arch/xilinx/mul_unsigned.ys
new file mode 100644
index 000000000..62495b90c
--- /dev/null
+++ b/tests/arch/xilinx/mul_unsigned.ys
@@ -0,0 +1,11 @@
+read_verilog mul_unsigned.v
+hierarchy -top mul_unsigned
+proc
+
+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
diff --git a/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys
new file mode 100644
index 000000000..821d0fab7
--- /dev/null
+++ b/tests/arch/xilinx/mux.ys
@@ -0,0 +1,45 @@
+read_verilog ../common/mux.v
+design -save read
+
+hierarchy -top mux2
+proc
+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 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 +/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 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 +/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 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 +/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 mux16 # Constrain all select calls below inside the top module
+select -assert-count 5 t:LUT6
+
+select -assert-none t:LUT6 %% t:* %D
diff --git a/tests/arch/xilinx/pmgen_xilinx_srl.ys b/tests/arch/xilinx/pmgen_xilinx_srl.ys
new file mode 100644
index 000000000..ea2f20487
--- /dev/null
+++ b/tests/arch/xilinx/pmgen_xilinx_srl.ys
@@ -0,0 +1,57 @@
+read_verilog -icells <<EOT
+module \$__XILINX_SHREG_ (input C, input D, input [31:0] L, input E, output Q, output SO);
+  parameter DEPTH = 1;
+  parameter [DEPTH-1:0] INIT = 0;
+  parameter CLKPOL = 1;
+  parameter ENPOL = 2;
+
+  wire pos_clk = C == CLKPOL;
+  reg pos_en;
+  always @(E)
+    if (ENPOL == 2) pos_en = 1'b1;
+    else pos_en = (E == ENPOL[0]);
+
+  reg [DEPTH-1:0] r;
+  always @(posedge pos_clk)
+    if (pos_en)
+      r <= {r[DEPTH-2:0], D};
+
+  assign Q = r[L];
+  assign SO = r[DEPTH-1];
+endmodule
+EOT
+read_verilog +/xilinx/cells_sim.v
+proc
+design -save model
+
+test_pmgen -generate xilinx_srl.fixed
+hierarchy -top pmtest_xilinx_srl_pm_fixed
+flatten; opt_clean
+
+design -save gold
+xilinx_srl -fixed
+techmap -autoproc -map %model
+design -stash gate
+
+design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed
+design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed
+dff2dffe -unmap # sat does not support flops-with-enable yet
+miter -equiv -flatten -make_assert gold gate miter
+sat -set-init-zero -seq 5 -verify -prove-asserts miter
+
+design -load model
+
+test_pmgen -generate xilinx_srl.variable
+hierarchy -top pmtest_xilinx_srl_pm_variable
+flatten; opt_clean
+
+design -save gold
+xilinx_srl -variable
+techmap -autoproc -map %model
+design -stash gate
+
+design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable
+design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable
+dff2dffe -unmap # sat does not support flops-with-enable yet
+miter -equiv -flatten -make_assert gold gate miter
+sat -set-init-zero -seq 5 -verify -prove-asserts miter
diff --git a/tests/arch/xilinx/run-test.sh b/tests/arch/xilinx/run-test.sh
new file mode 100755
index 000000000..bf19b887d
--- /dev/null
+++ b/tests/arch/xilinx/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/xilinx/shifter.ys b/tests/arch/xilinx/shifter.ys
new file mode 100644
index 000000000..455437f18
--- /dev/null
+++ b/tests/arch/xilinx/shifter.ys
@@ -0,0 +1,11 @@
+read_verilog ../common/shifter.v
+hierarchy -top top
+proc
+flatten
+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 top # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:BUFG
+select -assert-count 8 t:FDRE
+select -assert-none t:BUFG t:FDRE %% t:* %D
diff --git a/tests/arch/xilinx/tribuf.ys b/tests/arch/xilinx/tribuf.ys
new file mode 100644
index 000000000..4697703ca
--- /dev/null
+++ b/tests/arch/xilinx/tribuf.ys
@@ -0,0 +1,12 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+tribuf
+flatten
+synth
+equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # 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
+# TODO :: Tristate logic not yet supported; see https://github.com/YosysHQ/yosys/issues/1225
+select -assert-count 1 t:$_TBUF_
+select -assert-none t:$_TBUF_ %% t:* %D
diff --git a/tests/arch/xilinx/xilinx_srl.v b/tests/arch/xilinx/xilinx_srl.v
new file mode 100644
index 000000000..bc2a15ab2
--- /dev/null
+++ b/tests/arch/xilinx/xilinx_srl.v
@@ -0,0 +1,40 @@
+module xilinx_srl_static_test(input i, clk, output [1:0] q);
+reg head = 1'b0;
+reg [3:0] shift1 = 4'b0000;
+reg [3:0] shift2 = 4'b0000;
+
+always @(posedge clk) begin
+    head <= i;
+    shift1 <= {shift1[2:0], head};
+    shift2 <= {shift2[2:0], head};
+end
+
+assign q = {shift2[3], shift1[3]};
+endmodule
+
+module xilinx_srl_variable_test(input i, clk, input [1:0] l1, l2, output [1:0] q);
+reg head = 1'b0;
+reg [3:0] shift1 = 4'b0000;
+reg [3:0] shift2 = 4'b0000;
+
+always @(posedge clk) begin
+    head <= i;
+    shift1 <= {shift1[2:0], head};
+    shift2 <= {shift2[2:0], head};
+end
+
+assign q = {shift2[l2], shift1[l1]};
+endmodule
+
+module $__XILINX_SHREG_(input C, D, E, input [1:0] L, output Q);
+parameter CLKPOL = 1;
+parameter ENPOL = 1;
+parameter DEPTH = 1;
+parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
+reg [DEPTH-1:0] r = INIT;
+wire clk = C ^ CLKPOL;
+always @(posedge C)
+    if (E) 
+        r <= { r[DEPTH-2:0], D };
+assign Q = r[L];
+endmodule
diff --git a/tests/arch/xilinx/xilinx_srl.ys b/tests/arch/xilinx/xilinx_srl.ys
new file mode 100644
index 000000000..b8df0e55a
--- /dev/null
+++ b/tests/arch/xilinx/xilinx_srl.ys
@@ -0,0 +1,67 @@
+read_verilog xilinx_srl.v
+design -save read
+
+design -copy-to model $__XILINX_SHREG_
+hierarchy -top xilinx_srl_static_test
+prep
+design -save gold
+
+techmap
+xilinx_srl -fixed
+opt
+
+# stat
+# show -width
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 2 t:$__XILINX_SHREG_
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
+prep
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+dump gate
+sat -verify -prove-asserts -show-ports -seq 5 miter
+
+#design -load gold
+#stat
+
+#design -load gate
+#stat
+
+##########
+
+design -load read
+design -copy-to model $__XILINX_SHREG_
+hierarchy -top xilinx_srl_variable_test
+prep
+design -save gold
+
+xilinx_srl -variable
+opt
+
+#stat
+# show -width
+# write_verilog -noexpr -norename
+select -assert-count 1 t:$dff
+select -assert-count 1 t:$dff r:WIDTH=1 %i
+select -assert-count 2 t:$__XILINX_SHREG_
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
+prep
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 5 miter
+
+# design -load gold
+# stat
+
+# design -load gate
+# stat