Verilog: size casts are assignments

Size casts act like assignments, and hence, use the assignment conversion.

Author: kroening

CHANGELOG

@@ -1,5 +1,7 @@
 # EBMC 5.8
 
+* SystemVerilog: semantics fix for size casts
+
 # EBMC 5.7
 
 * Verilog: --initial-zero changes the default value from nondet to zero

regression/verilog/expressions/size_cast3.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 size_cast3.sv
 --module main
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This is not yet implemented.

src/verilog/verilog_expr.h

@@ -2554,12 +2554,6 @@ class verilog_explicit_size_cast_exprt : public binary_exprt
   {
     return op1();
   }
-
-  // lower to typecast
-  exprt lower() const
-  {
-    return typecast_exprt{op(), type()};
-  }
 };
 
 inline const verilog_explicit_size_cast_exprt &

src/verilog/verilog_lowering.cpp

@@ -480,7 +480,12 @@ exprt verilog_lowering(exprt expr)
   }
   else if(expr.id() == ID_verilog_explicit_size_cast)
   {
-    return to_verilog_explicit_size_cast_expr(expr).lower();
+    // These act like an assignment, and hence, the type checker
+    // has already converted the argument to the target type.
+    auto &size_cast = to_verilog_explicit_size_cast_expr(expr);
+    DATA_INVARIANT(
+      size_cast.op().type() == size_cast.type(), "size cast type consistency");
+    return size_cast.op();
   }
   else if(
     expr.id() == ID_verilog_streaming_concatenation_left_to_right ||

src/verilog/verilog_typecheck_expr.cpp

@@ -3319,6 +3319,11 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
         << "cannot perform size cast on " << to_string(op_type);
     }
 
+    // These act like an assignment (1800-2017 6.24.1)
+    assignment_conversion(expr.rhs(), expr.type());
+
+    CHECK_RETURN(expr.rhs().type() == expr.type());
+
     return std::move(expr);
   }
   else if(