diff --git a/regression/verilog/generate/generate-inst3.desc b/regression/verilog/generate/generate-inst3.desc
index f3480aeb7..a1c536cd5 100644
--- a/regression/verilog/generate/generate-inst3.desc
+++ b/regression/verilog/generate/generate-inst3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 generate-inst3.sv
 --bound 0
 ^\[main\.property1\] always main\.out == main\.in: PROVED up to bound 0$
@@ -6,4 +6,5 @@ generate-inst3.sv
 ^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.
diff --git a/regression/verilog/generate/genvar_scope1.desc b/regression/verilog/generate/genvar_scope1.desc
index 59b275e8d..53652164e 100644
--- a/regression/verilog/generate/genvar_scope1.desc
+++ b/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.
diff --git a/regression/verilog/generate/genvar_scope1.sv b/regression/verilog/generate/genvar_scope1.sv
index 0dc0013ae..e54ab7151 100644
--- a/regression/verilog/generate/genvar_scope1.sv
+++ b/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
diff --git a/regression/verilog/generate/genvar_scope2.desc b/regression/verilog/generate/genvar_scope2.desc
new file mode 100644
index 000000000..2d48fb073
--- /dev/null
+++ b/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.
diff --git a/regression/verilog/generate/genvar_scope2.sv b/regression/verilog/generate/genvar_scope2.sv
new file mode 100644
index 000000000..1ce55bdac
--- /dev/null
+++ b/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
diff --git a/regression/verilog/generate/genvar_scope3.desc b/regression/verilog/generate/genvar_scope3.desc
new file mode 100644
index 000000000..d01c614ce
--- /dev/null
+++ b/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.
diff --git a/regression/verilog/generate/genvar_scope3.sv b/regression/verilog/generate/genvar_scope3.sv
new file mode 100644
index 000000000..ac271ec5d
--- /dev/null
+++ b/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
diff --git a/regression/verilog/generate/genvar_scope4.desc b/regression/verilog/generate/genvar_scope4.desc
new file mode 100644
index 000000000..00da00dd6
--- /dev/null
+++ b/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.
diff --git a/regression/verilog/generate/genvar_scope4.sv b/regression/verilog/generate/genvar_scope4.sv
new file mode 100644
index 000000000..37878f42e
--- /dev/null
+++ b/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
diff --git a/regression/verilog/generate/genvar_scope5.desc b/regression/verilog/generate/genvar_scope5.desc
new file mode 100644
index 000000000..293dc9cd8
--- /dev/null
+++ b/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.
diff --git a/regression/verilog/generate/genvar_scope5.sv b/regression/verilog/generate/genvar_scope5.sv
new file mode 100644
index 000000000..f688a5e8b
--- /dev/null
+++ b/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
diff --git a/regression/verilog/generate/genvar_scope6.desc b/regression/verilog/generate/genvar_scope6.desc
new file mode 100644
index 000000000..ffebc0b2a
--- /dev/null
+++ b/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.
diff --git a/regression/verilog/generate/genvar_scope6.sv b/regression/verilog/generate/genvar_scope6.sv
new file mode 100644
index 000000000..dd2560ce3
--- /dev/null
+++ b/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
diff --git a/regression/verilog/generate/genvar_scope7.desc b/regression/verilog/generate/genvar_scope7.desc
new file mode 100644
index 000000000..1181e5984
--- /dev/null
+++ b/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.
diff --git a/regression/verilog/generate/genvar_scope7.sv b/regression/verilog/generate/genvar_scope7.sv
new file mode 100644
index 000000000..43015fda8
--- /dev/null
+++ b/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
diff --git a/regression/verilog/generate/genvar_scope8.desc b/regression/verilog/generate/genvar_scope8.desc
new file mode 100644
index 000000000..870f63480
--- /dev/null
+++ b/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.
diff --git a/regression/verilog/generate/genvar_scope8.sv b/regression/verilog/generate/genvar_scope8.sv
new file mode 100644
index 000000000..f08270ad1
--- /dev/null
+++ b/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
diff --git a/src/verilog/verilog_elaborate_module_instances.cpp b/src/verilog/verilog_elaborate_module_instances.cpp
index dc0f5f424..49508115d 100644
--- a/src/verilog/verilog_elaborate_module_instances.cpp
+++ b/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);
   }
 }
 
diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h
index a0825902a..9e54560f4 100644
--- a/src/verilog/verilog_expr.h
+++ b/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]);
diff --git a/src/verilog/verilog_generate.cpp b/src/verilog/verilog_generate.cpp
index 1203891de..a5997c698 100644
--- a/src/verilog/verilog_generate.cpp
+++ b/src/verilog/verilog_generate.cpp
@@ -64,7 +64,8 @@ Function: verilog_typecheckt::elaborate_generate_decl
 
 void verilog_typecheckt::elaborate_generate_decl(
   const verilog_generate_declt &generate_decl,
-  module_itemst &)
+  module_itemst &,
+  bool loop_local)
 {
   symbolt symbol{irep_idt{}, verilog_genvar_typet{}, mode};
 
@@ -85,9 +86,20 @@ void verilog_typecheckt::elaborate_generate_decl(
     symbol.name = hierarchical_identifier(symbol.base_name);
     symbol.pretty_name = strip_verilog_root_prefix(symbol.name);
 
-    genvars[symbol.base_name] = -1;
-
-    add_symbol(symbol);
+    // A genvar that is declared in the header of a loop generate construct
+    // is local to that loop (1800-2017 27.4), and hence is not added to
+    // the scope that contains the loop. Its state is tracked in the genvars
+    // map, together with the scope of that loop, and references to it are
+    // resolved using that map. We still report a clash with a symbol that
+    // is already present in the scope that contains the loop.
+    if(loop_local && symbol_table.lookup(symbol.name) == nullptr)
+      genvars[symbol.base_name] =
+        genvart{-1, hierarchical_identifier(irep_idt{})};
+    else
+    {
+      genvars[symbol.base_name] = genvart{-1, irep_idt{}};
+      add_symbol(symbol);
+    }
 
     // When used in a for loop, these come with an initial value.
     if(declarator.has_value())
@@ -100,7 +112,7 @@ void verilog_typecheckt::elaborate_generate_decl(
           << "must not assign negative value to genvar";
       }
 
-      genvars[symbol.base_name] = rhs;
+      genvars[symbol.base_name].value = rhs;
     }
   }
 }
@@ -140,9 +152,16 @@ verilog_typecheckt::module_itemst verilog_typecheckt::elaborate_generate_item(
     // generate variables.
     verilog_set_genvarst set_genvars(module_item);
     irept &variables = set_genvars.add("variables");
+    irept &loop_scopes = set_genvars.add("loop_scopes");
 
     for(const auto &it : genvars)
-      variables.set(it.first, integer2string(it.second));
+    {
+      variables.set(it.first, integer2string(it.second.value));
+
+      // Remember the scope of the loop a genvar is local to, if any.
+      if(it.second.is_loop_local())
+        loop_scopes.set(it.first, it.second.loop_scope);
+    }
 
     dest = elaborate_level({set_genvars});
   }
@@ -286,8 +305,8 @@ void verilog_typecheckt::elaborate_generate_assign(
     throw errort().with_location(statement.rhs().source_location())
       << "must not assign negative value to genvar";
   }
-  
-  it->second=rhs;
+
+  it->second.value = rhs;
 }
 
 /*******************************************************************\
@@ -339,7 +358,27 @@ void verilog_typecheckt::elaborate_generate_for(
   const verilog_generate_fort &for_statement,
   module_itemst &dest)
 {
-  elaborate_generate_item(for_statement.init(), dest);
+  // A genvar that is declared in the header of the loop generate construct
+  // is local to that loop, 1800-2017 27.4. Remember the state of the genvars
+  // it shadows, to restore it once the loop has been elaborated.
+  std::vector<std::pair<irep_idt, std::optional<genvart>>> shadowed_genvars;
+
+  if(for_statement.init().id() == ID_verilog_generate_decl)
+  {
+    auto &generate_decl = to_verilog_generate_decl(for_statement.init());
+
+    for(auto &declarator : generate_decl.declarators())
+    {
+      auto base_name = declarator.base_name();
+      auto it = genvars.find(base_name);
+      shadowed_genvars.emplace_back(
+        base_name, it == genvars.end() ? std::optional<genvart>{} : it->second);
+    }
+
+    elaborate_generate_decl(generate_decl, dest, true);
+  }
+  else
+    elaborate_generate_item(for_statement.init(), dest);
 
   // work out what the loop index is
   auto loop_index = generate_for_loop_index(for_statement.init());
@@ -398,4 +437,13 @@ void verilog_typecheckt::elaborate_generate_for(
       }
     }
   }
+
+  // The genvars that are declared in the loop header now go out of scope.
+  for(auto &[base_name, shadowed] : shadowed_genvars)
+  {
+    if(shadowed.has_value())
+      genvars[base_name] = *shadowed;
+    else
+      genvars.erase(base_name);
+  }
 }
diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
index 03a482474..9af3c5760 100644
--- a/src/verilog/verilog_typecheck.cpp
+++ b/src/verilog/verilog_typecheck.cpp
@@ -1618,6 +1618,34 @@ void verilog_typecheckt::convert_statement(
 
 /*******************************************************************\
 
+Function: verilog_typecheckt::build_genvars
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+verilog_typecheckt::genvarst
+verilog_typecheckt::build_genvars(const verilog_set_genvarst &set_genvars)
+{
+  genvarst genvars;
+
+  for(auto &var : set_genvars.variables())
+    genvars[var.first].value = string2integer(var.second.id_string());
+
+  // The genvars that are local to a loop generate construct come with
+  // the scope of that loop. 1800-2017 27.4.
+  for(auto &var : set_genvars.loop_scopes())
+    genvars[var.first].loop_scope = var.second.id();
+
+  return genvars;
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheckt::convert_module_item
 
   Inputs:
@@ -1707,10 +1735,7 @@ void verilog_typecheckt::convert_module_item(
   }
   else if(module_item.id() == ID_set_genvars)
   {
-    genvars.clear();
-    const auto &variables = to_verilog_set_genvars(module_item).variables();
-    for(auto &var : variables)
-      genvars[id2string(var.first)] = string2integer(var.second.id_string());
+    genvars = build_genvars(to_verilog_set_genvars(module_item));
 
     if(module_item.operands().size()!=1)
     {
@@ -1818,7 +1843,15 @@ void verilog_typecheckt::preresolve_identifiers(exprt &expr)
         auto &identifier_expr = to_verilog_identifier_expr(node);
         auto base_name = identifier_expr.base_name();
         auto symbol_ptr = resolve(base_name);
-        if(symbol_ptr != nullptr)
+        auto genvar = genvar_lookup(base_name);
+
+        if(genvar.has_value() && genvar->shadows(symbol_ptr))
+        {
+          // A genvar that is local to a loop generate construct, 1800-2017
+          // 27.4. These do not have a symbol, and are resolved when the
+          // expression is converted.
+        }
+        else if(symbol_ptr != nullptr)
         {
           identifier_expr.preresolved(symbol_ptr->name);
         }
diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h
index befe1a86e..f8c0ba395 100644
--- a/src/verilog/verilog_typecheck.h
+++ b/src/verilog/verilog_typecheck.h
@@ -257,21 +257,29 @@ class verilog_typecheckt:
   void elaborate_generate_if(const verilog_generate_ift &, module_itemst &dest);
   void
   elaborate_case_generate(const verilog_case_generatet &, module_itemst &dest);
-  void elaborate_generate_decl(const verilog_generate_declt &, module_itemst &);
+  // When loop_local is true, the genvar is declared in the header of a
+  // loop generate construct, and hence is local to that loop.
+  void elaborate_generate_decl(
+    const verilog_generate_declt &,
+    module_itemst &,
+    bool loop_local = false);
   void
   elaborate_generate_for(const verilog_generate_fort &, module_itemst &dest);
   exprt
   generate_for_loop_index(const verilog_module_itemt &initialization) const;
 
   // generate state
-  typedef std::map<irep_idt, mp_integer> genvarst;
+  typedef std::map<irep_idt, genvart> genvarst;
   genvarst genvars;
 
-  mp_integer genvar_value(const irep_idt &identifier) override
+  // The genvar environment that is recorded in a set_genvars module item.
+  static genvarst build_genvars(const verilog_set_genvarst &);
+
+  std::optional<genvart> genvar_lookup(const irep_idt &identifier) override
   {
-    genvarst::const_iterator it=genvars.find(identifier);
-    if(it==genvars.end())
-      return -1;
+    genvarst::const_iterator it = genvars.find(identifier);
+    if(it == genvars.end())
+      return {};
     else
       return it->second;
   }
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 878354c38..92182b443 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -1679,6 +1679,61 @@ exprt verilog_typecheck_exprt::convert_nullary_expr(nullary_exprt expr)
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::genvar_constant
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt verilog_typecheck_exprt::genvar_constant(
+  const irep_idt &base_name,
+  const source_locationt &source_location)
+{
+  auto genvar_opt = genvar_lookup(base_name);
+
+  // Genvars are declared without a value, and hence may be unset.
+  if(!genvar_opt.has_value() || genvar_opt->value < 0)
+    throw errort().with_location(source_location) << "invalid genvar value";
+
+  auto &value = genvar_opt->value;
+  std::size_t bits = address_bits(value + 1);
+
+  return from_integer(value, unsignedbv_typet{bits})
+    .with_source_location(source_location);
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_exprt::genvart::shadows
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool verilog_typecheck_exprt::genvart::shadows(const symbolt *symbol) const
+{
+  // A genvar that is declared separately from the loop generate construct
+  // has a symbol of its own, which is found by resolve.
+  if(!is_loop_local())
+    return false;
+
+  // A loop-local genvar shadows anything that is not declared inside the
+  // loop. Note that a clash with a symbol in the scope that contains the
+  // loop is rejected when the genvar is declared.
+  return symbol == nullptr ||
+         !has_prefix(id2string(symbol->name), id2string(loop_scope));
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::resolve
 
   Inputs:
@@ -1809,6 +1864,15 @@ exprt verilog_typecheck_exprt::convert_verilog_identifier(
   else
   {
     symbol = resolve(base_name);
+
+    // A genvar that is declared in the header of a loop generate construct
+    // is local to that loop, 1800-2017 27.4. It does not have a symbol of
+    // its own, and takes precedence over any symbol that is visible from
+    // the scope that contains the loop.
+    auto genvar = genvar_lookup(base_name);
+
+    if(genvar.has_value() && genvar->shadows(symbol))
+      return genvar_constant(base_name, expr.source_location());
   }
 
   if(symbol != nullptr)
@@ -1825,20 +1889,7 @@ exprt verilog_typecheck_exprt::convert_verilog_identifier(
     else if(symbol->type.id() == ID_verilog_genvar)
     {
       // This must be a constant.
-      mp_integer int_value = genvar_value(base_name);
-
-      if(int_value<0)
-      {
-        throw errort().with_location(expr.source_location())
-          << "invalid genvar value";
-      }
-
-      std::size_t bits = address_bits(int_value + 1);
-      source_locationt source_location=expr.source_location();
-
-      exprt result=from_integer(int_value, unsignedbv_typet(bits));
-      result.add_source_location()=source_location;
-      return result;
+      return genvar_constant(base_name, expr.source_location());
     }
     else if(
       symbol->type.id() == ID_verilog_sva_named_sequence ||
diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h
index 579b2f71b..fa912f5c3 100644
--- a/src/verilog/verilog_typecheck_expr.h
+++ b/src/verilog/verilog_typecheck_expr.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "sva_expr.h"
 #include "verilog_typecheck_base.h"
 
+#include <optional>
 #include <stack>
 
 class function_call_exprt;
@@ -128,12 +129,47 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 
   ranget convert_range(const exprt &range);
 
-  // to be overridden
-  virtual mp_integer genvar_value(const irep_idt &identifier)
+  // The state of a genvar during elaboration.
+  struct genvart
   {
-    PRECONDITION(false);
+    genvart() = default;
+
+    genvart(mp_integer _value, irep_idt _loop_scope)
+      : value(std::move(_value)), loop_scope(std::move(_loop_scope))
+    {
+    }
+
+    // The current value; negative when the genvar is not set yet.
+    mp_integer value = -1;
+
+    // When the genvar is declared in the header of a loop generate
+    // construct, it is local to that loop (1800-2017 27.4), and this is
+    // the prefix of the identifiers in the scope that contains the loop.
+    // The prefix is empty for a genvar that is declared separately from
+    // the loop, and hence is not local to any loop.
+    irep_idt loop_scope;
+
+    bool is_loop_local() const
+    {
+      return !loop_scope.empty();
+    }
+
+    // Does this genvar shadow the given symbol, which may be nullptr?
+    // A loop-local genvar shadows any symbol that is not declared inside
+    // the loop, i.e., any symbol in the scope that contains the loop or
+    // in a scope that encloses it.
+    bool shadows(const symbolt *) const;
+  };
+
+  // The genvar with the given base name, if any. To be overridden.
+  virtual std::optional<genvart> genvar_lookup(const irep_idt &)
+  {
+    return {};
   }
 
+  // Turn the value of a genvar into a constant.
+  exprt genvar_constant(const irep_idt &base_name, const source_locationt &);
+
   virtual void elaborate_symbol_rec(irep_idt)
   {
     PRECONDITION(false);