From 2d21017eaa5d6021b968ac3aecd607b4dfa5eef8 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 19 Dec 2025 07:54:48 -0800
Subject: [PATCH] Verilog: grammar for instance arrays

This adds the grammar to parse module instantiations that use an instance
array.  The type checker errors these as unsupported.
---
 regression/verilog/modules/instance_array1.desc |  6 +++---
 src/hw_cbmc_irep_ids.h                          |  1 +
 src/verilog/parser.y                            | 13 ++++++++++---
 src/verilog/verilog_expr.h                      | 10 ++++++++++
 src/verilog/verilog_interfaces.cpp              |  6 ++++++
 5 files changed, 30 insertions(+), 6 deletions(-)

diff --git a/regression/verilog/modules/instance_array1.desc b/regression/verilog/modules/instance_array1.desc
index 60b3153ff..c17213797 100644
--- a/regression/verilog/modules/instance_array1.desc
+++ b/regression/verilog/modules/instance_array1.desc
@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 instance_array1.sv
 
-^EXIT=0$
+^file .* line 9: no support for instance arrays$
+^EXIT=2$
 ^SIGNAL=0$
 --
 --
-This doesn't parse.
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 3478822e9..47e9b6b0b 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -128,6 +128,7 @@ IREP_ID_ONE(verilog_declarations)
 IREP_ID_ONE(verilog_default_clocking)
 IREP_ID_ONE(verilog_default_disable)
 IREP_ID_ONE(verilog_identifier)
+IREP_ID_ONE(verilog_instance_array)
 IREP_ID_ONE(verilog_interconnect)
 IREP_ID_ONE(verilog_lifetime)
 IREP_ID_ONE(verilog_logical_equality)
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index b45e98306..00f0b2823 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -3198,12 +3198,19 @@ hierarchical_instance_brace:
 
 hierarchical_instance:
 	  name_of_instance '(' list_of_module_connections_opt ')'
-		{ init($$, ID_inst); addswap($$, ID_base_name, $1); swapop($$, $3); }
+		{ $$ = $1; swapop($$, $3); }
 	;
 
 name_of_instance:
-	  { init($$, "$_&#ANON" + PARSER.get_next_id());}
-	| TOK_NON_TYPE_IDENTIFIER
+		/* Optional */
+		{ init($$, ID_inst);
+		  stack_expr($$).set(ID_base_name, "$_&#ANON" + PARSER.get_next_id());
+		}
+	| TOK_NON_TYPE_IDENTIFIER unpacked_dimension_brace
+		{ init($$, ID_inst);
+		  addswap($$, ID_base_name, $1);
+		  addswap($$, ID_verilog_instance_array, $2);
+		}
 	;
 
 list_of_module_connections_opt:
diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h
index b04681c33..6f86f95be 100644
--- a/src/verilog/verilog_expr.h
+++ b/src/verilog/verilog_expr.h
@@ -903,6 +903,16 @@ class verilog_inst_baset : public verilog_module_itemt
              connections.front().id() == ID_named_port_connection;
     }
 
+    const typet &instance_array() const
+    {
+      return static_cast<const typet &>(find(ID_verilog_instance_array));
+    }
+
+    typet &instance_array()
+    {
+      return static_cast<typet &>(add(ID_verilog_instance_array));
+    }
+
   protected:
     using exprt::operands;
   };
diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp
index 47169a64f..ac0c9ecf3 100644
--- a/src/verilog/verilog_interfaces.cpp
+++ b/src/verilog/verilog_interfaces.cpp
@@ -177,6 +177,12 @@ void verilog_typecheckt::interface_inst(
   const verilog_inst_baset &statement,
   const verilog_instt::instancet &op)
 {
+  if(op.instance_array().is_not_nil())
+  {
+    throw errort().with_location(op.source_location())
+      << "no support for instance arrays";
+  }
+
   bool primitive=statement.id()==ID_inst_builtin;
   const exprt &range_expr = static_cast<const exprt &>(op.find(ID_range));