6 files changed, 61 insertions, 32 deletions
diff --git a/tests/ice40/adffs.v b/tests/ice40/adffs.v
index 93c8bf52c..09dc36001 100644
--- a/tests/ice40/adffs.v
+++ b/tests/ice40/adffs.v
@@ -22,29 +22,25 @@ module adffn
             q <= d;
 endmodule
 
-module dffsr
+module dffs
     ( input d, clk, pre, clr, output reg q );
     initial begin
       q = 0;
     end
-	always @( posedge clk, posedge pre, posedge clr )
-		if ( clr )
-			q <= 1'b0;
-		else if ( pre )
+	always @( posedge clk, posedge pre )
+		if ( pre )
 			q <= 1'b1;
 		else
             q <= d;
 endmodule
 
-module ndffnsnr
+module ndffnr
     ( input d, clk, pre, clr, output reg q );
     initial begin
       q = 0;
     end
-	always @( negedge clk, negedge pre, negedge clr )
-		if ( !clr )
-			q <= 1'b0;
-		else if ( !pre )
+	always @( negedge clk, negedge pre )
+		if ( !pre )
 			q <= 1'b1;
 		else
             q <= d;
@@ -58,7 +54,7 @@ input a,
 output b,b1,b2,b3
 );
 
-dffsr u_dffsr (
+dffs u_dffs (
         .clk (clk ),
         .clr (clr),
         .pre (pre),
@@ -66,7 +62,7 @@ dffsr u_dffsr (
         .q (b )
     );
 
-ndffnsnr u_ndffnsnr (
+ndffnr u_ndffnr (
         .clk (clk ),
         .clr (clr),
         .pre (pre),
diff --git a/tests/ice40/adffs.ys b/tests/ice40/adffs.ys
index 14b251c5c..548060b66 100644
--- a/tests/ice40/adffs.ys
+++ b/tests/ice40/adffs.ys
@@ -1,12 +1,11 @@
 read_verilog adffs.v
 proc
-async2sync # converts async flops to a 'sync' variant clocked by a 'super'-clock
 flatten
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
+equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
-select -assert-count 1 t:SB_DFF
-select -assert-count 1 t:SB_DFFN
-select -assert-count 2 t:SB_DFFSR
-select -assert-count 7 t:SB_LUT4
-select -assert-none t:SB_DFF t:SB_DFFN t:SB_DFFSR t:SB_LUT4 %% t:* %D
+select -assert-count 1 t:SB_DFFNS
+select -assert-count 2 t:SB_DFFR
+select -assert-count 1 t:SB_DFFS
+select -assert-count 2 t:SB_LUT4
+select -assert-none t:SB_DFFNS t:SB_DFFR t:SB_DFFS t:SB_LUT4 %% t:* %D
diff --git a/tests/ice40/div_mod.ys b/tests/ice40/div_mod.ys
index 21cac7144..821d6c301 100644
--- a/tests/ice40/div_mod.ys
+++ b/tests/ice40/div_mod.ys
@@ -4,6 +4,6 @@ flatten
 equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
-select -assert-count 62 t:SB_LUT4
+select -assert-count 59 t:SB_LUT4
 select -assert-count 41 t:SB_CARRY
 select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D
diff --git a/tests/ice40/macc.v b/tests/ice40/macc.v
index 6c3676c83..6f68e7500 100644
--- a/tests/ice40/macc.v
+++ b/tests/ice40/macc.v
@@ -13,13 +13,35 @@ reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c;
 assign c = reg_tmp_c;
 always @(posedge clk)
 begin
-if(set)
-begin
-reg_tmp_c <= 0;
+    if(set)
+    begin
+        reg_tmp_c <= 0;
+    end
+    else
+    begin
+        reg_tmp_c <= a * b + c;
+    end
 end
-else
+endmodule
+
+module top2(clk,a,b,c,hold);
+parameter A_WIDTH = 6 /*4*/;
+parameter B_WIDTH = 6 /*3*/;
+input hold;
+input clk;
+input signed [(A_WIDTH - 1):0] a;
+input signed [(B_WIDTH - 1):0] b;
+output signed [(A_WIDTH + B_WIDTH - 1):0] c;
+reg signed [A_WIDTH-1:0] reg_a;
+reg signed [B_WIDTH-1:0] reg_b;
+reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c;
+assign c = reg_tmp_c;
+always @(posedge clk)
 begin
-reg_tmp_c <= a * b + c;
-end
+    if (!hold) begin
+        reg_a <= a;
+        reg_b <= b;
+        reg_tmp_c <= reg_a * reg_b + c;
+    end
 end
 endmodule
diff --git a/tests/ice40/macc.ys b/tests/ice40/macc.ys
index 0f4c19be5..fd30e79c5 100644
--- a/tests/ice40/macc.ys
+++ b/tests/ice40/macc.ys
@@ -1,13 +1,25 @@
 read_verilog macc.v
 proc
+design -save read
+
 hierarchy -top top
-#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_MAC16
+select -assert-none t:SB_MAC16 %% t:* %D
+
+design -load read
+hierarchy -top top2
 
-equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 -dsp
-async2sync
-equiv_opt -run prove: -assert null
+#equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+
+equiv_opt -run :prove -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+clk2fflogic
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -set-init-zero -seq 4 -verify -prove-asserts -show-ports miter
 
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd top # Constrain all select calls below inside the top module
+cd top2 # Constrain all select calls below inside the top module
 select -assert-count 1 t:SB_MAC16
 select -assert-none t:SB_MAC16 %% t:* %D
diff --git a/tests/ice40/run-test.sh b/tests/ice40/run-test.sh
index 2c72ca3a9..46716f9a0 100755
--- a/tests/ice40/run-test.sh
+++ b/tests/ice40/run-test.sh
@@ -6,7 +6,7 @@ for x in *.ys; do
 	echo "all:: run-$x"
 	echo "run-$x:"
 	echo "	@echo 'Running $x..'"
-	echo "	@../../yosys -ql ${x%.ys}.log $x -w 'Yosys has only limited support for tri-state logic at the moment.'"
+	echo "	@../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x"
 done
 for s in *.sh; do
 	if [ "$s" != "run-test.sh" ]; then