SystemVerilog: associative arrays

diffblue · Jan 14, 2025 · 542afcd · 542afcd
1 parent cbad677
commit 542afcd
Show file tree

Hide file tree

Showing 5 changed files with 38 additions and 5 deletions.
diff --git a/regression/verilog/data-types/associative_array1.desc b/regression/verilog/data-types/associative_array1.desc
@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 associative_array1.sv
 
-^EXIT=0$
+^no properties$
+^EXIT=10$
 ^SIGNAL=0$
 --
 --
-Parsing fails.
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -78,6 +78,7 @@ IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
 IREP_ID_ONE(verilog_array_range)
 IREP_ID_ONE(verilog_assignment_pattern)
+IREP_ID_ONE(verilog_associative_array)
 IREP_ID_ONE(verilog_declarations)
 IREP_ID_ONE(verilog_lifetime)
 IREP_ID_ONE(verilog_logical_equality)

diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -2004,6 +2004,24 @@ packed_dimension:
 	| unsized_dimension
 	;
 
+associative_dimension:
+	  '[' data_type ']'
+		{ init($$, ID_verilog_associative_array);
+		  // for the element type
+		  stack_type($$).add_subtype().make_nil();
+		}
+	| '[' '*' ']'
+		{ init($$, ID_verilog_associative_array);
+		  // for the element type
+		  stack_type($$).add_subtype().make_nil();
+		}
+	| "[*" ']'
+		{ init($$, ID_verilog_associative_array);
+		  // for the element type
+		  stack_type($$).add_subtype().make_nil();
+		}
+	;
+
 unpacked_dimension:
 	  '[' const_expression TOK_COLON const_expression ']'
 		{ init($$, ID_verilog_unpacked_array);
@@ -2022,6 +2040,7 @@ unpacked_dimension:
 variable_dimension:
 	  unsized_dimension
 	| unpacked_dimension
+	| associative_dimension
 	;
 
 variable_dimension_brace:

diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp
@@ -210,6 +210,13 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
         return rec;
     }
   }
+  else if(src.id() == ID_verilog_associative_array)
+  {
+    // The subtype is the element type.
+    auto tmp = to_type_with_subtype(src);
+    tmp.subtype() = elaborate_type(tmp.subtype());
+    return std::move(tmp);
+  }
   else if(src.id() == ID_verilog_byte)
   {
     // two-valued type, signed

diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp
@@ -33,10 +33,16 @@ typet verilog_declaratort::merged_type(const typet &declaration_type) const
   typet result = type();
   typet *p = &result;
 
-  while(p->id() == ID_verilog_unpacked_array)
+  while(p->id() == ID_verilog_unpacked_array ||
+        p->id() == ID_verilog_associative_array)
+  {
     p = &to_type_with_subtype(*p).subtype();
+  }
+
+  DATA_INVARIANT(
+    p->is_nil(),
+    "merged_type only works on unpacked arrays and associative arrays");
 
-  DATA_INVARIANT(p->is_nil(), "merged_type only works on unpacked arrays");
   *p = declaration_type;
 
   return result;