From 4f351810f962c178046b2b5e600215322a89df09 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 10 Jun 2025 09:25:54 -0700
Subject: [PATCH] Verilog: fix for named generate block scopes

Verilog generate blocks may be named, which creates a scope.
---
 CHANGELOG                              | 1 +
 regression/verilog/typedef/typedef2.sv | 7 +++++++
 src/verilog/parser.y                   | 9 ++++++---
 3 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG b/CHANGELOG
index 287d9252f..7130395fd 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,6 +1,7 @@
 # EBMC 5.7
 
 * Verilog: `elsif preprocessor directive
+* Verilog: fix for named generate blocks
 * LTL/SVA to Buechi with --buechi
 
 # EBMC 5.6
diff --git a/regression/verilog/typedef/typedef2.sv b/regression/verilog/typedef/typedef2.sv
index 2d395d1ee..135d3930b 100644
--- a/regression/verilog/typedef/typedef2.sv
+++ b/regression/verilog/typedef/typedef2.sv
@@ -23,6 +23,13 @@ module main();
     end
   endtask
 
+  // module item inside a named generate block
+  if (1) begin: some_block
+    typedef logic some_type;
+    some_type some_var;
+   end // checks
+
+  // named procedural block
   always @my_type2_var begin : named_block
     typedef bit my_type5;
     my_type5 my_type5_var;
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index bd55c56d1..58c71b13c 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -3163,9 +3163,12 @@ generate_block:
 	  generate_item
 	| TOK_BEGIN generate_item_brace TOK_END
 		{ init($$, ID_generate_block); swapop($$, $2); }
-	| TOK_BEGIN TOK_COLON generate_block_identifier generate_item_brace TOK_END
-		{ init($$, ID_generate_block);
-		  swapop($$, $4);
+	| TOK_BEGIN TOK_COLON generate_block_identifier
+		{ push_scope(stack_expr($3).id(), ".", verilog_scopet::BLOCK); }
+	  generate_item_brace TOK_END
+		{ pop_scope();
+		  init($$, ID_generate_block);
+		  swapop($$, $5);
 		  stack_expr($$).set(ID_base_name, stack_expr($3).id()); }
 	;