Verilog: $typename

This implements SystemVerilog's $typename system function.

Author: kroening

regression/verilog/system-functions/typename1.desc

@@ -0,0 +1,7 @@
+CORE
+typename1.sv
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/typename1.sv

@@ -0,0 +1,16 @@
+module main;
+
+  bit some_bit;
+  bit [31:0] vector1;
+  bit [0:31] vector2;
+  bit signed [31:0] vector3;
+
+  assert final ($typename(some_bit)=="bit");
+  assert final ($typename(vector1)=="bit[31:0]");
+  assert final ($typename(vector2)=="bit[0:31]");
+  assert final ($typename(vector3)=="bit signed[31:0]");
+
+  // $typename yields an elaboration-time constant
+  parameter P = $typename(some_bit);
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -664,6 +664,45 @@ constant_exprt verilog_typecheck_exprt::high(const exprt &expr)
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::typename_string
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
+{
+  auto &type = expr.type();
+
+  auto left = this->left(expr);
+  auto right = this->right(expr);
+
+  std::string s;
+
+  if(type.id() == ID_unsignedbv || type.id() == ID_verilog_unsignedbv)
+  {
+    s = "bit[" + to_string(left) + ":" + to_string(right) + "]";
+  }
+  else if(type.id() == ID_bool)
+  {
+    s = "bit";
+  }
+  else if(type.id() == ID_signedbv || type.id() == ID_verilog_signedbv)
+  {
+    s = "bit signed[" + to_string(left) + ":" + to_string(right) + "]";
+  }
+  else
+    s = "?";
+
+  return convert_constant(constant_exprt{s, string_typet{}});
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::convert_system_function
 
   Inputs:
@@ -866,6 +905,16 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
+  else if(identifier == "$typename")
+  {
+    if(arguments.size() != 1)
+    {
+      throw errort().with_location(expr.source_location())
+        << "$typename takes one argument";
+    }
+
+    return typename_string(arguments[0]);
+  }
   else
   {
     throw errort().with_location(expr.function().source_location())

src/verilog/verilog_typecheck_expr.h

@@ -196,6 +196,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   constant_exprt low(const exprt &);
   constant_exprt high(const exprt &);
   constant_exprt increment(const exprt &);
+  exprt typename_string(const exprt &);
 };
 
 bool verilog_typecheck(