Merge pull request #1 from YosysHQ/Sergey/tests_ice40

tests_ice40 improvements

17 files changed, 89 insertions, 136 deletions

diff --git a/tests/ice40/.gitignore b/tests/ice40/.gitignore
index 397b4a762..1d329c933 100644
--- a/tests/ice40/.gitignore
+++ b/tests/ice40/.gitignore
@@ -1 +1,2 @@
 *.log
+/run-test.mk
diff --git a/tests/ice40/add_sub.ys b/tests/ice40/add_sub.ys
index 84f31ec53..4a998d98d 100644
--- a/tests/ice40/add_sub.ys
+++ b/tests/ice40/add_sub.ys
@@ -1,7 +1,6 @@
 read_verilog add_sub.v
 hierarchy -top top
-synth -flatten -run coarse # technology-independent coarse grained synthesis
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
+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
diff --git a/tests/ice40/adffs.v b/tests/ice40/adffs.v
index af7022c79..93c8bf52c 100644
--- a/tests/ice40/adffs.v
+++ b/tests/ice40/adffs.v
@@ -22,16 +22,6 @@ module adffn
             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
-
 module dffsr
     ( input d, clk, pre, clr, output reg q );
     initial begin
@@ -65,7 +55,7 @@ input clk,
 input clr,
 input pre,
 input a,
-output b,b1,b2,b3,b4
+output b,b1,b2,b3
 );
 
 dffsr u_dffsr (
@@ -98,11 +88,4 @@ adffn u_adffn (
         .q (b3 )
     );
 
-dffe u_dffe (
-        .clk (clk ),
-        .en (clr),
-        .d (a ),
-        .q (b4 )
-    );
-
 endmodule
diff --git a/tests/ice40/adffs.ys b/tests/ice40/adffs.ys
index aee8cd6b4..14b251c5c 100644
--- a/tests/ice40/adffs.ys
+++ b/tests/ice40/adffs.ys
@@ -1,9 +1,12 @@
 read_verilog adffs.v
 proc
-dff2dffe
-synth_ice40
-select -assert-count 2 t:SB_DFFR
-select -assert-count 1 t:SB_DFFE
-select -assert-count 4 t:SB_LUT4
-#select -assert-none t:SB_LUT4 t:SB_DFFR t:SB_DFFE t:$_DFFSR_NPP_ t:$_DFFSR_PPP_ %% t:* %D
-write_verilog adffs_synth.v
+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
+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
diff --git a/tests/ice40/adffs_tb.v b/tests/ice40/adffs_tb.v
deleted file mode 100644
index e049edabc..000000000
--- a/tests/ice40/adffs_tb.v
+++ /dev/null
@@ -1,75 +0,0 @@
-module testbench;
-    reg clk;
-
-    initial begin
-        // $dumpfile("testbench.vcd");
-        // $dumpvars(0, testbench);
-
-        #5 clk = 0;
-        repeat (10000) begin
-            #5 clk = 1;
-            #5 clk = 0;
-        end
-
-        $display("OKAY");
-    end
-
-
-    reg [2:0] dinA = 0;
-    wire doutB,doutB1,doutB2,doutB3,doutB4;
-	reg dff,ndff,adff,adffn,dffe = 0;
-
-    top uut (
-        .clk (clk ),
-        .a (dinA[0] ),
-        .pre (dinA[1] ),
-        .clr (dinA[2] ),
-        .b (doutB ),
-        .b1 (doutB1 ),
-        .b2 (doutB2 )
-    );
-
-    always @(posedge clk) begin
-    #3;
-    dinA <= dinA + 1;
-    end
-
-	always @( posedge clk, posedge dinA[1], posedge dinA[2] )
-		if ( dinA[2] )
-			dff <= 1'b0;
-		else if ( dinA[1] )
-			dff <= 1'b1;
-		else
-            dff <= dinA[0];
-
-    always @( negedge clk, negedge dinA[1], negedge dinA[2] )
-		if ( !dinA[2] )
-			ndff <= 1'b0;
-		else if ( !dinA[1] )
-			ndff <= 1'b1;
-		else
-            ndff <= dinA[0];
-
-    always @( posedge clk, posedge dinA[2] )
-		if ( dinA[2] )
-			adff <= 1'b0;
-		else
-            adff <= dinA[0];
-
-    always @( posedge clk, negedge dinA[2] )
-		if ( !dinA[2] )
-			adffn <= 1'b0;
-		else
-            adffn <= dinA[0];
-
-    always @( posedge clk )
-		if ( dinA[2] )
-            dffe <= dinA[0];
-
-	assert_dff dff_test(.clk(clk), .test(doutB), .pat(dff));
-    assert_dff ndff_test(.clk(clk), .test(doutB1), .pat(ndff));
-    assert_dff adff_test(.clk(clk), .test(doutB2), .pat(adff));
-    //assert_dff adffn_test(.clk(clk), .test(doutB3), .pat(adffn));
-    //assert_dff dffe_test(.clk(clk), .test(doutB4), .pat(dffe));
-
-endmodule
diff --git a/tests/ice40/dffs.v b/tests/ice40/dffs.v
index d57c8c97c..d97840c43 100644
--- a/tests/ice40/dffs.v
+++ b/tests/ice40/dffs.v
@@ -1,5 +1,37 @@
-module top
+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
+
+module top (
+input clk,
+input en,
+input a,
+output b,b1,
+);
+
+dff u_dff (
+        .clk (clk ),
+        .d (a ),
+        .q (b )
+    );
+
+dffe u_ndffe (
+        .clk (clk ),
+        .en (en),
+        .d (a ),
+        .q (b1 )
+    );
+
+endmodule
diff --git a/tests/ice40/dffs.ys b/tests/ice40/dffs.ys
index 0fa0bc3eb..ee7f884b1 100644
--- a/tests/ice40/dffs.ys
+++ b/tests/ice40/dffs.ys
@@ -1,11 +1,10 @@
 read_verilog dffs.v
+hierarchy -top top
 proc
 flatten
-dff2dffe
-hierarchy -top top
-synth -flatten -run coarse # technology-independent coarse grained synthesis
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
+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 1 t:SB_DFF
-select -assert-none t:SB_DFF %% t:* %D
+select -assert-count 1 t:SB_DFFE
+select -assert-none t:SB_DFF t:SB_DFFE %% t:* %D
diff --git a/tests/ice40/div_mod.ys b/tests/ice40/div_mod.ys
index 93285cede..96753b4ef 100644
--- a/tests/ice40/div_mod.ys
+++ b/tests/ice40/div_mod.ys
@@ -1,7 +1,7 @@
 read_verilog div_mod.v
 hierarchy -top top
-synth -flatten -run coarse # technology-independent coarse grained synthesis
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
+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 88 t:SB_LUT4
diff --git a/tests/ice40/latches.ys b/tests/ice40/latches.ys
index 0abd7f195..fe0d1f70e 100644
--- a/tests/ice40/latches.ys
+++ b/tests/ice40/latches.ys
@@ -1,5 +1,6 @@
 read_verilog latches.v
 synth_ice40
-select -assert-count 5 t:SB_LUT4
-#select -assert-none t:SB_LUT4 %% t:* %D
+cd top
+select -assert-count 4 t:SB_LUT4
+select -assert-none t:SB_LUT4 %% t:* %D
 write_verilog latches_synth.v
diff --git a/tests/ice40/latches_tb.v b/tests/ice40/latches_tb.v
index 47ae8670c..b0585264b 100644
--- a/tests/ice40/latches_tb.v
+++ b/tests/ice40/latches_tb.v
@@ -10,8 +10,6 @@ module testbench;
             #5 clk = 1;
             #5 clk = 0;
         end
-
-        $display("OKAY");
     end
 
 
diff --git a/tests/ice40/memory.ys b/tests/ice40/memory.ys
index a0391e93d..9b7490cd8 100644
--- a/tests/ice40/memory.ys
+++ b/tests/ice40/memory.ys
@@ -1,4 +1,18 @@
 read_verilog memory.v
-synth_ice40
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+memory
+opt -full
+
+# TODO
+#equiv_opt -run prove: -assert null
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#sat -verify -prove-asserts -tempinduct -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
 write_verilog memory_synth.v
diff --git a/tests/ice40/memory_tb.v b/tests/ice40/memory_tb.v
index 5905f3ddd..be69374eb 100644
--- a/tests/ice40/memory_tb.v
+++ b/tests/ice40/memory_tb.v
@@ -10,8 +10,6 @@ module testbench;
             #5 clk = 1;
             #5 clk = 0;
         end
-
-        $display("OKAY");
     end
 
 
diff --git a/tests/ice40/mul.v b/tests/ice40/mul.v
index c099db0d9..d5b48b1d7 100644
--- a/tests/ice40/mul.v
+++ b/tests/ice40/mul.v
@@ -1,10 +1,9 @@
 module top
 (
- input [3:0] x,
- input [3:0] y,
+ input [5:0] x,
+ input [5:0] y,
 
- output [3:0] A,
- output [3:0] B
+ output [11:0] A,
  );
 
 assign A =  x * y;
diff --git a/tests/ice40/mul.ys b/tests/ice40/mul.ys
index 35048d14a..8a0822a84 100644
--- a/tests/ice40/mul.ys
+++ b/tests/ice40/mul.ys
@@ -1,9 +1,7 @@
 read_verilog mul.v
 hierarchy -top top
-synth -flatten -run coarse # technology-independent coarse grained synthesis
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check same as technology-dependent fine-grained synthesis
+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 15 t:SB_LUT4
-select -assert-count 3 t:SB_CARRY
-select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D
+select -assert-count 1 t:SB_MAC16
+select -assert-none t:SB_MAC16 %% t:* %D
diff --git a/tests/ice40/mux.ys b/tests/ice40/mux.ys
index 9e3d87b7f..182b49499 100644
--- a/tests/ice40/mux.ys
+++ b/tests/ice40/mux.ys
@@ -1,6 +1,8 @@
 read_verilog mux.v
-synth_ice40
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40
-design -load postopt
-select -assert-count 20 t:SB_LUT4
-select -assert-count 1 t:SB_CARRY
+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 19 t:SB_LUT4
+select -assert-none t:SB_LUT4 %% t:* %D
diff --git a/tests/ice40/run-test.sh b/tests/ice40/run-test.sh
index 5bd9fb173..90a8a3c83 100755
--- a/tests/ice40/run-test.sh
+++ b/tests/ice40/run-test.sh
@@ -12,14 +12,14 @@ for x in *.ys; do
 	echo "all:: run-$x"
 	echo "run-$x:"
 	echo "	@echo 'Running $x..'"
-	echo "	@../../yosys -ql ${x%.ys}.log $x"
+	echo "	@../../yosys -ql ${x%.ys}.log $x -w 'Yosys has only limited support for tri-state logic at the moment.'"
 done
 for t in *_tb.v; do
 	echo "all:: run-$t"
 	echo "run-$t:"
 	echo "	@echo 'Running $t..'"
-	echo "	@iverilog -o ${t%_tb.v}_testbench  $t ${t%_tb.v}_synth.v common.v $COMMON_PREFIX/simcells.v $TECHLIBS_PREFIX/ice40/cells_sim.v"
-	echo "	@if ! vvp -N ${t%_tb.v}_testbench > ${t%_tb.v}_testbench.log 2>&1; then grep 'ERROR' ${t%_tb.v}_testbench.log; exit 0; elif grep 'ERROR' ${t%_tb.v}_testbench.log || ! grep 'OKAY' ${t%_tb.v}_testbench.log; then echo "FAIL"; exit 0; fi"
+	echo "	@iverilog -o ${t%_tb.v}_testbench  $t ${t%_tb.v}_synth.v common.v $TECHLIBS_PREFIX/ice40/cells_sim.v"
+	echo "	@vvp -N ${t%_tb.v}_testbench"
 done
 for s in *.sh; do
 	if [ "$s" != "run-test.sh" ]; then
diff --git a/tests/ice40/tribuf.ys b/tests/ice40/tribuf.ys
index 9b7ea1eab..d1e1b3108 100644
--- a/tests/ice40/tribuf.ys
+++ b/tests/ice40/tribuf.ys
@@ -1,7 +1,8 @@
 read_verilog tribuf.v
 hierarchy -top top
-synth -flatten -run coarse # technology-independent coarse grained synthesis
-equiv_opt -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
+proc
+flatten
+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 top # Constrain all select calls below inside the top module
 select -assert-count 1 t:$_TBUF_