Adding tests for dynamic part select optimisation

diff --git a/tests/arch/common/dynamic_part_select/forloop_select.v b/tests/arch/common/dynamic_part_select/forloop_select.v
new file mode 100644 (file)
index 0000000..9276a3e
--- /dev/null
+++ b/tests/arch/common/dynamic_part_select/forloop_select.v
@@ -0,0 +1,19 @@
+module forloop_select #(parameter WIDTH=256, SELW=4)
+   (input                  clk ,
+    input [9:0]           ctrl ,
+    input [15:0]          din ,
+    input                 en,
+    output reg [WIDTH-1:0] dout);
+   
+   reg [SELW-1:0]         sel;
+   localparam SLICE = WIDTH/(SELW**2);
+   
+   always @(posedge clk)
+     begin
+        if (en) begin
+           for (sel = 0; sel < 4'hf; sel=sel+1'b1)
+             dout[(ctrl*sel)+:SLICE] <= din;
+        end
+     end
+endmodule
+

diff --git a/tests/arch/common/dynamic_part_select/multiple_blocking.v b/tests/arch/common/dynamic_part_select/multiple_blocking.v
new file mode 100644 (file)
index 0000000..7861722
--- /dev/null
+++ b/tests/arch/common/dynamic_part_select/multiple_blocking.v
@@ -0,0 +1,19 @@
+module multiple_blocking #(parameter WIDTH=256, SELW=2)
+   (input               clk ,
+    input [9:0]         ctrl ,
+    input [15:0]        din ,
+    input [SELW-1:0]    sel ,
+    output reg [WIDTH:0] dout);
+
+   localparam SLICE = WIDTH/(SELW**2);
+   reg [9:0]            a;
+   reg [SELW-1:0]       b;
+   reg [15:0]           c;
+   always @(posedge clk) begin
+      a = ctrl + 1;
+      b = sel - 1;
+      c = ~din;
+      dout = dout + 1;
+      dout[a*b+:SLICE] = c;
+   end
+endmodule

diff --git a/tests/arch/common/dynamic_part_select/nonblocking.v b/tests/arch/common/dynamic_part_select/nonblocking.v
new file mode 100644 (file)
index 0000000..89c3995
--- /dev/null
+++ b/tests/arch/common/dynamic_part_select/nonblocking.v
@@ -0,0 +1,14 @@
+module nonblocking #(parameter WIDTH=256, SELW=2)
+   (input                 clk ,
+    input [9:0]           ctrl ,
+    input [15:0]          din ,
+    input [SELW-1:0]      sel ,
+    output reg [WIDTH-1:0] dout);
+
+   localparam SLICE = WIDTH/(SELW**2);
+   always @(posedge clk) begin
+      dout <= dout + 1;
+      dout[ctrl*sel+:SLICE] <= din ;
+   end
+   
+endmodule

diff --git a/tests/arch/common/dynamic_part_select/original.v b/tests/arch/common/dynamic_part_select/original.v
new file mode 100644 (file)
index 0000000..bd7654e
--- /dev/null
+++ b/tests/arch/common/dynamic_part_select/original.v
@@ -0,0 +1,13 @@
+module original #(parameter WIDTH=256, SELW=2)
+   (input              clk ,
+    input [9:0]           ctrl ,
+    input [15:0]          din ,
+    input [SELW-1:0]      sel ,
+    output reg [WIDTH-1:0] dout);
+   
+   localparam SLICE = WIDTH/(SELW**2);
+   always @(posedge clk)
+     begin
+       dout[ctrl*sel+:SLICE] <= din ;
+     end
+endmodule

diff --git a/tests/arch/common/dynamic_part_select/reset_test.v b/tests/arch/common/dynamic_part_select/reset_test.v
new file mode 100644 (file)
index 0000000..5a3a9b9
--- /dev/null
+++ b/tests/arch/common/dynamic_part_select/reset_test.v
@@ -0,0 +1,24 @@
+module reset_test #(parameter WIDTH=256, SELW=2)
+   (input                  clk ,
+    input [9:0]           ctrl ,
+    input [15:0]          din ,
+    input [SELW-1:0]      sel ,
+    input wire                    reset,
+    output reg [WIDTH-1:0] dout);
+   
+   reg [5:0]              i;
+   wire [SELW-1:0]        rval = {reset, {SELW-1{1'b0}}};
+   localparam SLICE = WIDTH/(SELW**2);
+   // Doing exotic reset. masking 2 LSB bits to 0, 6 MSB bits to 1 for
+   // whatever reason.
+   always @(posedge clk) begin
+      if (reset) begin: reset_mask
+         for (i = 0; i < 16; i=i+1) begin
+            dout[i*rval+:SLICE] <= 32'hDEAD;
+         end
+      end
+      //else begin
+      dout[ctrl*sel+:SLICE] <= din;
+      //end
+   end
+endmodule

diff --git a/tests/arch/common/dynamic_part_select/reversed.v b/tests/arch/common/dynamic_part_select/reversed.v
new file mode 100644 (file)
index 0000000..6ef0e10
--- /dev/null
+++ b/tests/arch/common/dynamic_part_select/reversed.v
@@ -0,0 +1,13 @@
+module reversed #(parameter WIDTH=256, SELW=2)
+   (input                  clk ,
+    input [9:0]           ctrl ,
+    input [15:0]          din ,
+    input [SELW-1:0]      sel ,
+    output reg [WIDTH-1:0] dout);
+   
+   localparam SLICE = WIDTH/(SELW**2);
+   always @(posedge clk) begin
+      dout[(1024-ctrl*sel)-:SLICE] <= din;
+   end
+endmodule
+

diff --git a/tests/arch/xilinx/dynamic_part_select.ys b/tests/arch/xilinx/dynamic_part_select.ys
new file mode 100644 (file)
index 0000000..597229c
--- /dev/null
+++ b/tests/arch/xilinx/dynamic_part_select.ys
@@ -0,0 +1,59 @@
+#### Original testcase ###
+read_verilog ../common/dynamic_part_select/original.v
+hierarchy -top original
+prep -flatten -top original
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
+ 
+### Multiple blocking assingments ###
+read_verilog ../common/dynamic_part_select/multiple_blocking.v
+hierarchy -top multiple_blocking
+prep -flatten -top multiple_blocking
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
+ 
+### Non-blocking to the same output register ###
+read_verilog ../common/dynamic_part_select/nonblocking.v
+hierarchy -top nonblocking
+prep -flatten -top nonblocking
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
+
+### For-loop select, one dynamic input
+read_verilog ../common/dynamic_part_select/forloop_select.v
+hierarchy -top forloop_select
+prep -flatten -top forloop_select
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 5 -prove-skip 1 miter
+
+### Double loop (part-select, reset) ### 
+read_verilog ../common/dynamic_part_select/reset_test.v
+hierarchy -top reset_test
+prep -flatten -top reset_test
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
+
+### Reversed part-select case ###
+read_verilog ../common/dynamic_part_select/reversed.v
+hierarchy -top reversed
+prep -flatten -top reversed
+design -save gold
+ 
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -seq 20 -prove-skip 1 miter