SystemVerilog: string data type

This adds 1800-2017 6.16 string.
diffblue · kroening · Nov 21, 2024 · Jan 9, 2025 · 3fb4d16541439478b36e58b558dd6dce75b5f665
commit 3fb4d16541439478b36e58b558dd6dce75b5f665
diff --git a/CHANGELOG b/CHANGELOG
@@ -8,7 +8,7 @@
 * Verilog: fix for nor/nand/xnor primitive gates
 * SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits
 * SystemVerilog: $itor, $rtoi
-* SystemVerilog: chandle, event
+* SystemVerilog: chandle, event, string
 
 # EBMC 5.4
 

diff --git a/regression/verilog/data-types/string1.desc b/regression/verilog/data-types/string1.desc
@@ -0,0 +1,7 @@
+CORE
+string1.sv
+--bound 0
+^no properties$
+^EXIT=10$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/data-types/string1.sv b/regression/verilog/data-types/string1.sv
@@ -0,0 +1,7 @@
+module main;
+
+  // IEEE 1800-2017 6.16
+  string xyz;
+  string my_string = xyz;
+
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -108,6 +108,7 @@ IREP_ID_ONE(verilog_chandle)
 IREP_ID_ONE(verilog_null)
 IREP_ID_ONE(verilog_event)
 IREP_ID_ONE(verilog_event_trigger)
+IREP_ID_ONE(verilog_string)
 IREP_ID_ONE(reg)
 IREP_ID_ONE(macromodule)
 IREP_ID_ONE(output_register)

diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
@@ -1988,6 +1988,8 @@ std::string expr2verilogt::convert(const typet &type)
     return "logic";
   else if(type.id() == ID_verilog_integer)
     return "integer";
+  else if(type.id() == ID_verilog_string)
+    return "string";
   else if(type.id() == ID_verilog_reg)
     return "reg";
   else if(type.id() == ID_verilog_time)

diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -1475,7 +1475,7 @@ data_type:
 	          stack_expr($$).set(ID_identifier, id);
 	        }
 	| TOK_STRING
-	        { init($$, ID_string); }
+	        { init($$, ID_verilog_string); }
 	| TOK_CHANDLE
 	        { init($$, ID_verilog_chandle); }
 	| TOK_VIRTUAL interface_opt interface_identifier

diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp
@@ -379,6 +379,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
     return struct_union_typet{src.id(), std::move(components)}
       .with_source_location(src.source_location());
   }
+  else if(src.id() == ID_verilog_string)
+  {
+    return src;
+  }
   else if(src.id() == ID_type)
   {
     return src;

diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -761,6 +761,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
   {
     s = "event";
   }
+  else if(type.id() == ID_verilog_string)
+  {
+    s = "string";
+  }
   else
     s = "?";
 
@@ -2331,6 +2335,21 @@ typet verilog_typecheck_exprt::max_type(
   if(vt0.is_event() || vt1.is_null())
     return t0;
 
+  if(
+    vt0.is_string() && (vt1.is_signed() || vt1.is_unsigned() ||
+                        vt1.is_verilog_signed() || vt1.is_verilog_unsigned()))
+  {
+    return t0;
+  }
+
+  if(
+    (vt0.is_signed() || vt0.is_unsigned() || vt0.is_verilog_signed() ||
+     vt0.is_verilog_unsigned()) &&
+    vt0.is_string())
+  {
+    return t1;
+  }
+
   if(vt0.is_other() || vt1.is_other())
     return static_cast<const typet &>(get_nil_irep());
 

diff --git a/src/verilog/vtype.cpp b/src/verilog/vtype.cpp
@@ -83,6 +83,11 @@ vtypet::vtypet(const typet &type)
     vtype = EVENT;
     width = 32;
   }
+  else if(type.id() == ID_verilog_string)
+  {
+    vtype = STRING;
+    width = 0;
+  }
   else 
   {
     width=0;
@@ -136,6 +141,9 @@ std::ostream &operator << (std::ostream &out, const vtypet &vtype)
   case vtypet::EVENT:
     return out << "event";
 
+  case vtypet::STRING:
+    return out << "string";
+
   case vtypet::UNKNOWN:
   case vtypet::OTHER:
   default:

diff --git a/src/verilog/vtype.h b/src/verilog/vtype.h
@@ -43,6 +43,10 @@ class vtypet
   {
     return vtype == EVENT;
   }
+  bool is_string() const
+  {
+    return vtype == STRING;
+  }
   inline bool is_other() const { return vtype==OTHER; }
 
 protected:
@@ -59,6 +63,7 @@ class vtypet
     NULL_TYPE,
     CHANDLE,
     EVENT,
+    STRING,
     OTHER
   } _vtypet;
   _vtypet vtype;