Add torture test for (* nowrshmsk *) stride optimization

tests/various/dynamic_part_select.ys

@@ -69,6 +69,24 @@ design -copy-from gate -as gate gate
 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
 sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
 
+### For-loop select, one dynamic input, (* nowrshmsk *)
+design -reset
+read_verilog ./dynamic_part_select/forloop_select_nowrshmsk.v
+proc
+rename -top gold
+design -stash gold
+
+read_verilog ./dynamic_part_select/forloop_select_gate.v
+proc
+rename -top gate
+design -stash gate
+
+design -copy-from gold -as gold gold
+design -copy-from gate -as gate gate
+
+miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
+sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
+
 #### Double loop (part-select, reset) ### 
 design -reset
 read_verilog ./dynamic_part_select/reset_test.v

tests/various/dynamic_part_select/forloop_select_nowrshmsk.v

@@ -0,0 +1,20 @@
+`default_nettype none
+module forloop_select #(parameter WIDTH=16, SELW=4, CTRLW=$clog2(WIDTH), DINW=2**SELW)
+   (input wire             clk,
+    input wire [CTRLW-1:0] ctrl,
+    input wire [DINW-1:0]  din,
+    input wire             en,
+    (* nowrshmsk *)
+    output reg [WIDTH-1:0] dout);
+
+   reg [SELW: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