SystemVerilog: chandle data type

This adds 1800 2017 6.14 chandle.

Author: kroening

regression/verilog/data-types/chandle1.desc

@@ -0,0 +1,8 @@
+CORE
+chandle1.sv
+--bound 0
+^\[main\.p0\] always main\.some_handle == null: PROVED up to bound 0$
+^\[main\.p1\] always 56'h6368616E646C65 == 56'h6368616E646C65: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/verilog/data-types/chandle1.sv

@@ -0,0 +1,9 @@
+module main;
+
+  // IEEE 1800-2017 6.14
+  chandle some_handle = null;
+
+  p0: assert final (some_handle == null);
+  p1: assert final ($typename(some_handle) == "chandle");
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -103,7 +103,8 @@ IREP_ID_ONE(verilog_value_range)
 IREP_ID_ONE(verilog_void)
 IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)
 IREP_ID_ONE(verilog_streaming_concatenation_right_to_left)
-IREP_ID_ONE(chandle)
+IREP_ID_ONE(verilog_chandle)
+IREP_ID_ONE(verilog_null)
 IREP_ID_ONE(event)
 IREP_ID_ONE(reg)
 IREP_ID_ONE(macromodule)

src/verilog/Makefile

@@ -26,6 +26,7 @@ SRC = aval_bval_encoding.cpp \
       verilog_typecheck_base.cpp \
       verilog_typecheck_expr.cpp \
       verilog_typecheck_sva.cpp \
+      verilog_types.cpp \
       verilog_y.tab.cpp \
       vtype.cpp
 

src/verilog/expr2verilog.cpp

@@ -1208,6 +1208,15 @@ expr2verilogt::resultt expr2verilogt::convert_constant(
     ieee_float.from_expr(tmp);
     return {precedence, ieee_float.to_ansi_c_string()};
   }
+  else if(type.id() == ID_verilog_chandle)
+  {
+    if(src.get_value() == ID_NULL)
+    {
+      dest = "null";
+    }
+    else
+      return convert_norep(src, precedence);
+  }
   else
     return convert_norep(src, precedence);
 
@@ -1978,6 +1987,8 @@ std::string expr2verilogt::convert(const typet &type)
 
     return dest;
   }
+  else if(type.id() == ID_verilog_chandle)
+    return "chandle";
   else if(type.id() == ID_verilog_genvar)
     return "genvar";
   else if(type.id()==ID_integer)
@@ -1988,6 +1999,8 @@ std::string expr2verilogt::convert(const typet &type)
     return "real";
   else if(type.id()==ID_verilog_realtime)
     return "realtime";
+  else if(type.id() == ID_verilog_null)
+    return "null";
   else if(type.id() == ID_verilog_enum)
   {
     return "enum";

src/verilog/parser.y

@@ -1473,7 +1473,7 @@ data_type:
 	| TOK_STRING
 	        { init($$, ID_string); }
 	| TOK_CHANDLE
-	        { init($$, ID_chandle); }
+	        { init($$, ID_verilog_chandle); }
 	| TOK_VIRTUAL interface_opt interface_identifier
 	        { init($$, "virtual_interface"); }
 	| /*scope_opt*/ type_identifier packed_dimension_brace
@@ -4018,7 +4018,7 @@ primary:  primary_literal
 	| cast
 	| assignment_pattern_expression
 	| streaming_concatenation
-        | TOK_NULL { init($$, ID_NULL); }
+        | TOK_NULL { init($$, ID_verilog_null); }
         | TOK_THIS { init($$, ID_this); }
 	;
 

src/verilog/verilog_elaborate_type.cpp

@@ -337,6 +337,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
   {
     return src;
   }
+  else if(src.id() == ID_verilog_chandle)
+  {
+    return src;
+  }
   else
   {
     throw errort().with_location(source_location)

src/verilog/verilog_lowering.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include "aval_bval_encoding.h"
 #include "verilog_bits.h"
 #include "verilog_expr.h"
+#include "verilog_types.h"
 
 /// If applicable, lower the three Verilog real types to floatbv.
 typet lower_verilog_real_types(typet type)
@@ -183,9 +184,26 @@ exprt verilog_lowering(exprt expr)
       // no need to change value
       expr.type() = lower_verilog_real_types(expr.type());
     }
+    else if(expr.type().id() == ID_verilog_chandle)
+    {
+      // this is 'null'
+      return to_verilog_chandle_type(expr.type()).null_expr();
+    }
 
     return expr;
   }
+  else if(expr.id() == ID_symbol)
+  {
+    auto &symbol_expr = to_symbol_expr(expr);
+    if(expr.type().id() == ID_verilog_chandle)
+    {
+      auto &chandle_type = to_verilog_chandle_type(expr.type());
+      return symbol_exprt{
+        symbol_expr.get_identifier(), chandle_type.encoding()};
+    }
+    else
+      return expr;
+  }
   else if(expr.id() == ID_concatenation)
   {
     if(
@@ -421,6 +439,8 @@ typet verilog_lowering(typet type)
 {
   if(type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv)
     return lower_to_aval_bval(type);
+  else if(type.id() == ID_verilog_chandle)
+    return to_verilog_chandle_type(type).encoding();
   else
     return type;
 }

src/verilog/verilog_synthesis.cpp

@@ -3346,7 +3346,14 @@ void verilog_synthesist::synth_assignments(
   if(!symbol.is_state_var)
     post_process_wire(symbol.name, new_value);
 
-  equal_exprt equality_expr{symbol_expr(symbol, curr_or_next), new_value};
+  auto lhs = symbol_expr(symbol, curr_or_next);
+
+  if(lhs.type() != new_value.type())
+    throw errort() << lhs.pretty() << "\nVS\n" << new_value.pretty();
+  DATA_INVARIANT(
+    lhs.type() == new_value.type(), "synth_assignments type consistency");
+
+  equal_exprt equality_expr{std::move(lhs), new_value};
 
   constraints.add_to_operands(std::move(equality_expr));
 }

src/verilog/verilog_typecheck_expr.cpp

@@ -735,6 +735,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
   {
     s = "shortreal";
   }
+  else if(type.id() == ID_verilog_chandle)
+  {
+    s = "chandle";
+  }
   else
     s = "?";
 
@@ -1003,6 +1007,11 @@ exprt verilog_typecheck_exprt::convert_nullary_expr(nullary_exprt expr)
     throw errort().with_location(expr.source_location())
       << "'this' outside of method";
   }
+  else if(expr.id() == ID_verilog_null)
+  {
+    return constant_exprt{ID_NULL, typet{ID_verilog_null}}.with_source_location(
+      expr.source_location());
+  }
   else
   {
     throw errort().with_location(expr.source_location())
@@ -1932,6 +1941,17 @@ void verilog_typecheck_exprt::implicit_typecast(
       return;
     }
   }
+  else if(src_type.id() == ID_verilog_null)
+  {
+    if(dest_type.id() == ID_verilog_chandle)
+    {
+      if(expr.id() == ID_constant)
+      {
+        expr.type() = dest_type;
+        return;
+      }
+    }
+  }
 
   throw errort().with_location(expr.source_location())
     << "failed to convert `" << to_string(src_type) << "' to `"
@@ -2184,6 +2204,12 @@ typet verilog_typecheck_exprt::max_type(
   vtypet vt0=vtypet(t0);
   vtypet vt1=vtypet(t1);
 
+  if(vt0.is_null() || vt1.is_chandle())
+    return t1;
+
+  if(vt0.is_chandle() || vt1.is_null())
+    return t0;
+
   if(vt0.is_other() || vt1.is_other())
     return static_cast<const typet &>(get_nil_irep());