Verilog: loop-local genvar scoping

regression/verilog/generate/generate-inst3.desc

@@ -1,9 +1,10 @@
-KNOWNBUG
+CORE
 generate-inst3.sv
 --bound 0
 ^\[main\.property1\] always main\.out == main\.in: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-The parameter is not passed correctly.
+The genvar in the part selects of the port connections is evaluated per
+iteration of the loop.

regression/verilog/generate/genvar_scope1.desc

@@ -1,11 +1,12 @@
-KNOWNBUG
+CORE
 genvar_scope1.sv
-
-^no properties$
-^EXIT=10$
+--bound 0
+^\[main\.property\.p1\] always main\.some_wire1 == 16'h100: PROVED up to bound 0$
+^\[main\.property\.p2\] always main\.some_wire2 == 16'hB0A: PROVED up to bound 0$
+^EXIT=0$
 ^SIGNAL=0$
 --
 --
-A genvar declared in a loop generate construct header is not local to that
-loop, and hence the second loop yields "definition of symbol `gi' conflicts
-with earlier definition".
+A genvar declared in the header of a loop generate construct is local to that
+loop, and hence two loops in the same scope may both declare a genvar with the
+same name.

regression/verilog/generate/genvar_scope1.sv

@@ -4,14 +4,24 @@ module main;
   // header is local to that loop.  Two loops in the same scope may hence
   // both use the name gi.
 
+  wire [15:0] some_wire1, some_wire2;
+
   for (genvar gi = 0; gi < 2; gi++)
   begin : b1
     wire [7:0] w = gi;
+    assign some_wire1[gi*8 +: 8] = w;
   end
 
   for (genvar gi = 0; gi < 2; gi++)
   begin : b2
     wire [7:0] w = gi + 10;
+    assign some_wire2[gi*8 +: 8] = w;
   end
 
+  // main.b1[0].w is 0 and main.b1[1].w is 1
+  always assert p1: some_wire1 == 16'h0100;
+
+  // main.b2[0].w is 10 and main.b2[1].w is 11
+  always assert p2: some_wire2 == 16'h0b0a;
+
 endmodule

regression/verilog/generate/genvar_scope2.desc

@@ -0,0 +1,11 @@
+CORE
+genvar_scope2.sv
+--bound 0
+^\[main\.property\.p1\] always main\.some_wire1 == 16'h100: PROVED up to bound 0$
+^\[main\.property\.p2\] always main\.some_wire2 == 16'hB0A: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+A genvar that is declared separately from the loop generate construct is not
+local to any loop, and hence may be shared by two loops in the same scope.

regression/verilog/generate/genvar_scope2.sv

@@ -0,0 +1,27 @@
+module main;
+
+  // Per 1800-2017 27.4, a genvar that is declared separately from the loop
+  // generate construct is not local to any loop, and hence may be shared by
+  // two loops in the same scope.
+
+  wire [15:0] some_wire1, some_wire2;
+
+  genvar gi;
+
+  for (gi = 0; gi < 2; gi = gi + 1)
+  begin : b1
+    wire [7:0] w = gi;
+    assign some_wire1[gi*8 +: 8] = w;
+  end
+
+  for (gi = 0; gi < 2; gi = gi + 1)
+  begin : b2
+    wire [7:0] w = gi + 10;
+    assign some_wire2[gi*8 +: 8] = w;
+  end
+
+  always assert p1: some_wire1 == 16'h0100;
+
+  always assert p2: some_wire2 == 16'h0b0a;
+
+endmodule

regression/verilog/generate/genvar_scope3.desc

@@ -0,0 +1,10 @@
+CORE
+genvar_scope3.sv
+
+^file .* line 8: definition of symbol `gi' conflicts with earlier definition at line 6$
+^EXIT=2$
+^SIGNAL=0$
+--
+--
+A genvar declared in the header of a loop generate construct must not clash
+with a symbol in the enclosing scope.

regression/verilog/generate/genvar_scope3.sv

@@ -0,0 +1,13 @@
+module main;
+
+  // The genvar declared in the loop header is in the same scope as the
+  // wire, and hence this is a conflict.
+
+  wire gi;
+
+  for (genvar gi = 0; gi < 2; gi++)
+  begin : b1
+    wire w = 0;
+  end
+
+endmodule

regression/verilog/generate/genvar_scope4.desc

@@ -0,0 +1,10 @@
+CORE
+genvar_scope4.sv
+
+^file .* line 11: unknown identifier gi$
+^EXIT=2$
+^SIGNAL=0$
+--
+--
+A genvar declared in the header of a loop generate construct is not visible
+outside of that loop.

regression/verilog/generate/genvar_scope4.sv

@@ -0,0 +1,13 @@
+module main;
+
+  // Per 1800-2017 27.4, the genvar declared in the loop header is local to
+  // the loop, and hence is not visible after the loop.
+
+  for (genvar gi = 0; gi < 2; gi++)
+  begin : b1
+    wire w = 0;
+  end
+
+  localparam p = gi;
+
+endmodule

regression/verilog/generate/genvar_scope5.desc

@@ -0,0 +1,10 @@
+CORE
+genvar_scope5.sv
+--bound 0
+^\[main\.property\.p1\] always main\.some_wire == 16'h100: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+A genvar declared in the header of a loop generate construct shadows a symbol
+with the same name in a scope that encloses the loop.

regression/verilog/generate/genvar_scope5.sv

@@ -0,0 +1,20 @@
+module main;
+
+  // Per 1800-2017 27.4, the genvar declared in the loop header is local to
+  // the loop, and hence shadows the wire with the same name in the scope
+  // that encloses the loop.
+
+  wire [7:0] gi = 8'hff;
+  wire [15:0] some_wire;
+
+  if (1)
+  begin : outer
+    for (genvar gi = 0; gi < 2; gi++)
+    begin : inner
+      assign some_wire[gi*8 +: 8] = gi;
+    end
+  end
+
+  always assert p1: some_wire == 16'h0100;
+
+endmodule

regression/verilog/generate/genvar_scope6.desc

@@ -0,0 +1,11 @@
+CORE
+genvar_scope6.sv
+--bound 0
+^\[main\.property\.p1\] always main\.some_wire1 == 16'h100: PROVED up to bound 0$
+^\[main\.property\.p2\] always main\.some_wire2 == 16'hB0A: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+A genvar declared in the header of a loop generate construct shadows a
+localparam or a genvar with the same name in an enclosing scope.

regression/verilog/generate/genvar_scope6.sv

@@ -0,0 +1,32 @@
+module main;
+
+  // The genvar declared in the loop header shadows both the localparam and
+  // the genvar declared in the scope that encloses the loop, 1800-2017 27.4.
+
+  localparam gi = 8'hff;
+
+  wire [15:0] some_wire1, some_wire2;
+
+  if (1)
+  begin : outer1
+    for (genvar gi = 0; gi < 2; gi++)
+    begin : inner
+      assign some_wire1[gi*8 +: 8] = gi;
+    end
+  end
+
+  genvar gj;
+
+  if (1)
+  begin : outer2
+    for (genvar gj = 0; gj < 2; gj++)
+    begin : inner
+      assign some_wire2[gj*8 +: 8] = gj + 10;
+    end
+  end
+
+  always assert p1: some_wire1 == 16'h0100;
+
+  always assert p2: some_wire2 == 16'h0b0a;
+
+endmodule

regression/verilog/generate/genvar_scope7.desc

@@ -0,0 +1,10 @@
+CORE
+genvar_scope7.sv
+--bound 0
+^\[main\.property\.p1\] always main\.some_wire\[1:0\] == 2'b10: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Two nested loop generate constructs may both declare a genvar with the same
+name in their header.

regression/verilog/generate/genvar_scope7.sv

@@ -0,0 +1,18 @@
+module main;
+
+  // The genvar declared in the header of the inner loop is local to that
+  // loop, and hence shadows the genvar of the outer loop, 1800-2017 27.4.
+
+  wire [3:0] some_wire;
+
+  for (genvar i = 0; i < 2; i++)
+  begin : a
+    for (genvar i = 0; i < 2; i++)
+    begin : b
+      assign some_wire[i] = i == 1;
+    end
+  end
+
+  always assert p1: some_wire[1:0] == 2'b10;
+
+endmodule

regression/verilog/generate/genvar_scope8.desc

@@ -0,0 +1,10 @@
+CORE
+genvar_scope8.sv
+--bound 0
+^\[main\.property\.p1\] always main\.q == 4'b0010: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+A genvar declared in the header of a loop generate construct is in scope in the
+port connections and parameter values of a module instance.

regression/verilog/generate/genvar_scope8.sv

@@ -0,0 +1,26 @@
+module child(input i, output o);
+
+  parameter P = 0;
+
+  assign o = (P == 3) ? ~i : i;
+
+endmodule
+
+module main;
+
+  // The genvar declared in the loop header is local to the loop, 1800-2017
+  // 27.4, and must be resolvable in the port connections and the parameter
+  // values of a module instance, with the value it has in the given
+  // iteration of the loop.
+
+  wire [3:0] d = 4'b1010;
+  wire [3:0] q;
+
+  for (genvar g = 0; g < 4; g++)
+  begin : blk
+    child #(.P(g)) c(.i(d[g]), .o(q[g]));
+  end
+
+  always assert p1: q == 4'b0010;
+
+endmodule

src/verilog/verilog_elaborate_module_instances.cpp

@@ -162,8 +162,12 @@ void verilog_typecheckt::elaborate_module_instances(
   }
   else if(module_item.id() == ID_set_genvars)
   {
-    elaborate_module_instances(
-      to_verilog_set_genvars(module_item).module_item());
+    // Port connections may use genvars, which hence need to be in scope.
+    auto old_genvars = genvars;
+    auto &set_genvars = to_verilog_set_genvars(module_item);
+    genvars = build_genvars(set_genvars);
+    elaborate_module_instances(set_genvars.module_item());
+    genvars = std::move(old_genvars);
   }
 }
 
@@ -243,11 +247,12 @@ void verilog_typecheckt::process_parameter_override(
   }
   else if(item.id() == ID_set_genvars)
   {
-    for(auto &sub_item : item.operands())
-    {
-      if(sub_item.id() == ID_parameter_override)
-        process_parameter_override(to_verilog_parameter_override(sub_item));
-    }
+    // Parameter overrides may use genvars, which hence need to be in scope.
+    auto old_genvars = genvars;
+    auto &set_genvars = to_verilog_set_genvars(item);
+    genvars = build_genvars(set_genvars);
+    process_parameter_override(set_genvars.module_item());
+    genvars = std::move(old_genvars);
   }
 }
 
@@ -295,8 +300,12 @@ void verilog_typecheckt::parameterize_instantiated_modules(
   }
   else if(module_item.id() == ID_set_genvars)
   {
-    parameterize_instantiated_modules(
-      to_verilog_set_genvars(module_item).module_item());
+    // Parameter values may use genvars, which hence need to be in scope.
+    auto old_genvars = genvars;
+    auto &set_genvars = to_verilog_set_genvars(module_item);
+    genvars = build_genvars(set_genvars);
+    parameterize_instantiated_modules(set_genvars.module_item());
+    genvars = std::move(old_genvars);
   }
 }
 

src/verilog/verilog_expr.h

@@ -939,6 +939,18 @@ class verilog_set_genvarst : public verilog_module_itemt
     return find(ID_variables).get_named_sub();
   }
 
+  // The scope of the loop generate construct a genvar is local to,
+  // for those genvars that are local to a loop. 1800-2017 27.4.
+  named_subt &loop_scopes()
+  {
+    return add("loop_scopes").get_named_sub();
+  }
+
+  const named_subt &loop_scopes() const
+  {
+    return find("loop_scopes").get_named_sub();
+  }
+
   const verilog_module_itemt &module_item() const
   {
     return static_cast<const verilog_module_itemt &>(get_sub()[0]);