Adding tests for dynamic part select optimisation

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
+

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

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

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

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

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
+

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