Merge pull request #2133 from dh73/nodev_head

Adding latch tests for shift&mask AST dynamic part-select enhancements

tests/various/dynamic_part_select.ys

@@ -104,3 +104,59 @@ 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
+
+### Latches
+## Issue 1990
+design -reset
+read_verilog ./dynamic_part_select/latch_1990.v
+hierarchy -top latch_1990; prep; async2sync
+rename -top gold
+design -stash gold
+
+read_verilog ./dynamic_part_select/latch_1990_gate.v
+hierarchy -top latch_1990_gate; prep
+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 -show-public -verify -set-init-zero equiv
+
+###
+## Part select with obvious latch, expected to fail due comparison with old shift&mask AST transformation    
+design -reset
+read_verilog ./dynamic_part_select/latch_002.v
+hierarchy -top latch_002; prep; async2sync
+rename -top gold
+design -stash gold
+
+read_verilog ./dynamic_part_select/latch_002_gate.v
+hierarchy -top latch_002_gate; prep; async2sync
+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 -falsify -set-init-zero equiv
+
+## Part select + latch, with no shift&mask
+design -reset
+read_verilog ./dynamic_part_select/latch_002.v
+hierarchy -top latch_002; prep; async2sync
+rename -top gold
+design -stash gold
+
+read_verilog ./dynamic_part_select/latch_002_gate_good.v
+hierarchy -top latch_002_gate; prep; async2sync
+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

tests/various/dynamic_part_select/forloop_select.v

@@ -1,11 +1,12 @@
+`default_nettype none
 module forloop_select #(parameter WIDTH=16, SELW=4, CTRLW=$clog2(WIDTH), DINW=2**SELW)
-   (input                  clk,
+   (input wire             clk,
-    input [CTRLW-1:0] 	   ctrl,
+    input wire [CTRLW-1:0] ctrl,
-    input [DINW-1:0] 	   din,
+    input wire [DINW-1:0]  din,
-    input                  en,
+    input wire             en,
     output reg [WIDTH-1:0] dout);
 
-   reg [SELW:0] 	   sel;
+   reg [SELW:0]            sel;
    localparam SLICE = WIDTH/(SELW**2);
 
    always @(posedge clk)
@@ -16,4 +17,3 @@ module forloop_select #(parameter WIDTH=16, SELW=4, CTRLW=$clog2(WIDTH), DINW=2*
         end
      end
 endmodule
-

tests/various/dynamic_part_select/forloop_select_gate.v

@@ -1,8 +1,9 @@
+`default_nettype none
 module forloop_select_gate (clk, ctrl, din, en, dout);
-      input clk;
+      input wire clk;
-      input [3:0] ctrl;
+      input wire [3:0] ctrl;
-      input [15:0] din;
+      input wire [15:0] din;
-      input en;
+      input wire en;
       output reg [15:0] dout;
       reg [4:0] sel;
       always @(posedge clk)

tests/various/dynamic_part_select/latch_002.v

@@ -0,0 +1,13 @@
+`default_nettype none
+module latch_002
+  (dword, sel, st, vect);
+   output reg [63:0] dword;
+   input wire [7:0]  vect;
+   input wire [7:0]  sel;
+   input wire        st;
+   
+   always @(*) begin
+      if (st)
+	dword[8*sel +:8] <= vect[7:0];
+   end
+endmodule // latch_002

tests/various/dynamic_part_select/latch_002_gate.v

@@ -0,0 +1,18 @@
+`default_nettype none
+module latch_002_gate(dword, vect, sel, st);
+   output reg [63:0] dword;
+   input wire [7:0]  vect;
+   input wire [7:0]  sel;
+   input wire 	     st;
+   reg [63:0] 	     mask;
+   reg [63:0] 	     data;
+   always @*
+     case (|(st))
+       1'b 1:
+         begin
+            mask  = (8'b 11111111)<<((((8)*(sel)))+(0));
+            data  = ((8'b 11111111)&(vect[7:0]))<<((((8)*(sel)))+(0));
+            dword <= ((dword)&(~(mask)))|(data);
+         end
+     endcase
+endmodule

tests/various/dynamic_part_select/latch_002_gate_good.v

@@ -0,0 +1,141 @@
+`default_nettype none
+module latch_002_gate (dword, vect, sel, st);
+   output reg [63:0] dword;
+   input wire [7:0]  vect;
+   input wire [7:0]  sel;
+   input 	     st;
+   always @*
+     case (|(st))
+       1'b 1:
+         case ((((8)*(sel)))+(0))
+           0:
+             dword[7:0] <= vect[7:0];
+           1:
+             dword[8:1] <= vect[7:0];
+           2:
+             dword[9:2] <= vect[7:0];
+           3:
+             dword[10:3] <= vect[7:0];
+           4:
+             dword[11:4] <= vect[7:0];
+           5:
+             dword[12:5] <= vect[7:0];
+           6:
+             dword[13:6] <= vect[7:0];
+           7:
+             dword[14:7] <= vect[7:0];
+           8:
+             dword[15:8] <= vect[7:0];
+           9:
+             dword[16:9] <= vect[7:0];
+           10:
+             dword[17:10] <= vect[7:0];
+           11:
+             dword[18:11] <= vect[7:0];
+           12:
+             dword[19:12] <= vect[7:0];
+           13:
+             dword[20:13] <= vect[7:0];
+           14:
+             dword[21:14] <= vect[7:0];
+           15:
+             dword[22:15] <= vect[7:0];
+           16:
+             dword[23:16] <= vect[7:0];
+           17:
+             dword[24:17] <= vect[7:0];
+           18:
+             dword[25:18] <= vect[7:0];
+           19:
+             dword[26:19] <= vect[7:0];
+           20:
+             dword[27:20] <= vect[7:0];
+           21:
+             dword[28:21] <= vect[7:0];
+           22:
+             dword[29:22] <= vect[7:0];
+           23:
+             dword[30:23] <= vect[7:0];
+           24:
+             dword[31:24] <= vect[7:0];
+           25:
+             dword[32:25] <= vect[7:0];
+           26:
+             dword[33:26] <= vect[7:0];
+           27:
+             dword[34:27] <= vect[7:0];
+           28:
+             dword[35:28] <= vect[7:0];
+           29:
+             dword[36:29] <= vect[7:0];
+           30:
+             dword[37:30] <= vect[7:0];
+           31:
+             dword[38:31] <= vect[7:0];
+           32:
+             dword[39:32] <= vect[7:0];
+           33:
+             dword[40:33] <= vect[7:0];
+           34:
+             dword[41:34] <= vect[7:0];
+           35:
+             dword[42:35] <= vect[7:0];
+           36:
+             dword[43:36] <= vect[7:0];
+           37:
+             dword[44:37] <= vect[7:0];
+           38:
+             dword[45:38] <= vect[7:0];
+           39:
+             dword[46:39] <= vect[7:0];
+           40:
+             dword[47:40] <= vect[7:0];
+           41:
+             dword[48:41] <= vect[7:0];
+           42:
+             dword[49:42] <= vect[7:0];
+           43:
+             dword[50:43] <= vect[7:0];
+           44:
+             dword[51:44] <= vect[7:0];
+           45:
+             dword[52:45] <= vect[7:0];
+           46:
+             dword[53:46] <= vect[7:0];
+           47:
+             dword[54:47] <= vect[7:0];
+           48:
+             dword[55:48] <= vect[7:0];
+           49:
+             dword[56:49] <= vect[7:0];
+           50:
+             dword[57:50] <= vect[7:0];
+           51:
+             dword[58:51] <= vect[7:0];
+           52:
+             dword[59:52] <= vect[7:0];
+           53:
+             dword[60:53] <= vect[7:0];
+           54:
+             dword[61:54] <= vect[7:0];
+           55:
+             dword[62:55] <= vect[7:0];
+           56:
+             dword[63:56] <= vect[7:0];
+           57:
+             dword[63:57] <= vect[7:0];
+           58:
+             dword[63:58] <= vect[7:0];
+           59:
+             dword[63:59] <= vect[7:0];
+           60:
+             dword[63:60] <= vect[7:0];
+           61:
+             dword[63:61] <= vect[7:0];
+           62:
+             dword[63:62] <= vect[7:0];
+           63:
+             dword[63:63] <= vect[7:0];
+         endcase
+     endcase
+endmodule

tests/various/dynamic_part_select/latch_1990.v

@@ -0,0 +1,12 @@
+module latch_1990 #(
+        parameter BUG = 1
+) (
+	(* nowrshmsk = !BUG *)
+        output reg [1:0] x
+);
+        wire z = 0;
+        integer i;
+        always @*
+                for (i = 0; i < 2; i=i+1)
+                        x[z^i] = z^i;
+endmodule

tests/various/dynamic_part_select/latch_1990_gate.v

@@ -0,0 +1,6 @@
+`default_nettype none
+module latch_1990_gate
+  (output wire [1:0] x);
+   assign x = 2'b10;
+endmodule // latch_1990_gate
+

tests/various/dynamic_part_select/multiple_blocking.v

@@ -1,8 +1,9 @@
+`default_nettype none
 module multiple_blocking #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW)
-   (input                  clk,
+   (input wire             clk,
-    input [CTRLW-1:0] 	   ctrl,
+    input wire [CTRLW-1:0] ctrl,
-    input [DINW-1:0] 	   din,
+    input wire [DINW-1:0]  din,
-    input [SELW-1:0] 	   sel,
+    input wire [SELW-1:0]  sel,
     output reg [WIDTH-1:0] dout);
    
    localparam SLICE = WIDTH/(SELW**2);

tests/various/dynamic_part_select/multiple_blocking_gate.v

@@ -1,8 +1,9 @@
+`default_nettype none
 module multiple_blocking_gate (clk, ctrl, din, sel, dout);
-   input clk;
+   input wire clk;
-   input [4:0] ctrl;
+   input wire [4:0] ctrl;
-   input [1:0] din;
+   input wire [1:0] din;
-   input [0:0] sel;
+   input wire [0:0] sel;
    output reg [31:0] dout;
    reg [5:0] 	     a;
    reg [0:0] 	     b;

tests/various/dynamic_part_select/nonblocking.v

@@ -1,8 +1,9 @@
+`default_nettype none
 module nonblocking #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW)
-   (input                  clk,
+   (input wire             clk,
-    input [CTRLW-1:0] 	   ctrl,
+    input wire [CTRLW-1:0] ctrl,
-    input [DINW-1:0] 	   din,
+    input wire [DINW-1:0]  din,
-    input [SELW-1:0] 	   sel,
+    input wire [SELW-1:0]  sel,
     output reg [WIDTH-1:0] dout);
    
    localparam SLICE = WIDTH/(SELW**2);

tests/various/dynamic_part_select/nonblocking_gate.v

@@ -1,8 +1,9 @@
+`default_nettype none
 module nonblocking_gate (clk, ctrl, din, sel, dout);
-   input clk;
+   input wire clk;
-   input [4:0] ctrl;
+   input wire [4:0] ctrl;
-   input [1:0] din;
+   input wire [1:0] din;
-   input [0:0] sel;
+   input wire [0:0] sel;
    output reg [31:0] dout;
    always @(posedge clk)
      begin

tests/various/dynamic_part_select/original.v

@@ -1,8 +1,9 @@
+`default_nettype none
 module original #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW)
-   (input                  clk,
+   (input wire             clk,
-    input [CTRLW-1:0] 	   ctrl,
+    input wire [CTRLW-1:0] ctrl,
-    input [DINW-1:0] 	   din,
+    input wire [DINW-1:0]  din,
-    input [SELW-1:0] 	   sel,
+    input wire [SELW-1:0]  sel,
     output reg [WIDTH-1:0] dout);
    localparam SLICE = WIDTH/(SELW**2);
    always @(posedge clk)

tests/various/dynamic_part_select/original_gate.v

@@ -1,8 +1,9 @@
+`default_nettype none
 module original_gate (clk, ctrl, din, sel, dout);
-   input clk;
+   input wire clk;
-   input [4:0] ctrl;
+   input wire [4:0] ctrl;
-   input [1:0] din;
+   input wire [1:0] din;
-   input [0:0] sel;
+   input wire [0:0] sel;
    output reg [31:0] dout;
    always @(posedge clk)
      case (({(ctrl)*(sel)})+(0))

tests/various/dynamic_part_select/reset_test.v

@@ -1,8 +1,10 @@
+`default_nettype none
 module reset_test  #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW)
-   (input                  clk,
+   (input wire             clk,
-    input [CTRLW-1:0] 	   ctrl,
+    input wire             reset,
-    input [DINW-1:0] 	   din,
+    input wire [CTRLW-1:0] ctrl,
-    input [SELW-1:0] 	   sel,
+    input wire [DINW-1:0]  din,
+    input wire [SELW-1:0]  sel,
     output reg [WIDTH-1:0] dout);
    
    reg [SELW:0] 		   i;
@@ -16,8 +18,6 @@ module reset_test  #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SE
             dout[i*rval+:SLICE] <= 32'hDEAD;
          end
       end
-      //else begin
       dout[ctrl*sel+:SLICE] <= din;
-      //end
    end
 endmodule

tests/various/dynamic_part_select/reset_test_gate.v

@@ -1,8 +1,10 @@
-module reset_test_gate (clk, ctrl, din, sel, dout);
+`default_nettype none
-   input clk;
+module reset_test_gate (clk, reset, ctrl, din, sel, dout);
-   input [4:0] ctrl;
+   input wire clk;
-   input [1:0] din;
+   input wire reset;
-   input [0:0] sel;
+   input wire [4:0] ctrl;
+   input wire [1:0] din;
+   input wire [0:0] sel;
    output reg [31:0] dout;
    reg [1:0] 	     i;
    wire [0:0] 	     rval;

tests/various/dynamic_part_select/reversed.v

@@ -1,8 +1,9 @@
+`default_nettype none
 module reversed #(parameter WIDTH=32, SELW=4, CTRLW=$clog2(WIDTH), DINW=2**SELW)
-   (input                  clk,
+   (input wire             clk,
-    input [CTRLW-1:0] 	   ctrl,
+    input wire [CTRLW-1:0] ctrl,
-    input [DINW-1:0] 	   din,
+    input wire [DINW-1:0]  din,
-    input [SELW-1:0] 	   sel,
+    input wire [SELW-1:0]  sel,
     output reg [WIDTH-1:0] dout);
    
    localparam SLICE = WIDTH/(SELW**2);

tests/various/dynamic_part_select/reversed_gate.v

@@ -1,8 +1,9 @@
+`default_nettype none
 module reversed_gate (clk, ctrl, din, sel, dout);
-   input clk;
+   input wire clk;
-   input [4:0] ctrl;
+   input wire [4:0] ctrl;
-   input [15:0] din;
+   input wire [15:0] din;
-   input [3:0] 	sel;
+   input wire [3:0]  sel;
    output reg [31:0] dout;
    always @(posedge clk)
      case ((({(32)-((ctrl)*(sel))})+(1))-(2))