SystemVerilog: floating-point casts

Casts from real/shortreal/realtime to integers must use
round-to-nearest-ties-to-away.

The standard doesn't specify how to round int-to-float or double-to-single.
We use RNA for consistency.

Author: kroening

regression/verilog/expressions/cast_from_real1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE broken-smt-backend
 cast_from_real1.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Verilog casts from real to integer round, and do not truncate.

regression/verilog/expressions/cast_from_real1.sv

@@ -3,7 +3,12 @@ module main;
   always assert (integer'(1.0) == 1);
   always assert (integer'(-1.0) == -1);
 
-  // Casting rounds away from zero (1800-2017 6.12.2)
-  always assert (integer'(1.9) == 2);
+  // Casting rounds to nearest-ties-away-from zero (1800-2017 6.12.2)
+  // Examples from the standard.
+  always assert (integer'(35.7) == 36);
+  always assert (integer'(35.5) == 36);
+  always assert (integer'(35.2) == 35);
+  always assert (integer'(-1.5) == -2);
+  always assert (integer'(1.5) == 2);
 
 endmodule

regression/verilog/expressions/cast_to_real1.sv

@@ -1,11 +1,12 @@
 module main;
 
-  // no rounding
+  // No rounding.
   p0: assert final (real'(0) == 0.0);
   p1: assert final (real'(1) == 1.0);
 
-  // rounding, away from zero
+  // Rounding. The standard does not say how.  This is RNA.
+  // Icarus Verilog, Aldec Riviera, Questa, VCS agree.
+  // Cadence Xcelium disagrees.
   p2: assert final (real'('hffff_ffff_ffff_ffff) == real'('h1_0000_0000_0000_0000));
-  p3: assert final (real'(-'sh0_ffff_ffff_ffff_ffff) == real'(-'sh1_0000_0000_0000_0000));
 
 endmodule

regression/verilog/expressions/cast_to_real2.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 cast_to_real2.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Typechecking yields inconsistent types.

src/verilog/verilog_lowering.cpp

@@ -251,19 +251,44 @@ exprt verilog_lowering_cast(typecast_exprt expr)
   auto &src_type = expr.op().type();
   auto &dest_type = expr.type();
 
+  // float to int
+  if(
+    (src_type.id() == ID_verilog_real ||
+     src_type.id() == ID_verilog_shortreal ||
+     src_type.id() == ID_verilog_realtime || src_type.id() == ID_floatbv) &&
+    (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
+     dest_type.id() == ID_bool))
+  {
+    // 1800-2017 6.12.2 requires rounding away from zero when converting
+    // to integers.
+    auto rm = floatbv_rounding_mode(ieee_floatt::rounding_modet::ROUND_TO_AWAY);
+    auto rti =
+      floatbv_round_to_integral_exprt{expr.op(), rm}.with_source_location(
+        expr.source_location());
+    auto new_cast = floatbv_typecast_exprt{
+      rti,
+      ieee_floatt::rounding_mode_expr(
+        ieee_floatt::rounding_modet::ROUND_TO_ZERO),
+      verilog_lowering(dest_type)};
+    return std::move(new_cast);
+  }
+
+  // float to float, int to float
   if(
     dest_type.id() == ID_verilog_real ||
     dest_type.id() == ID_verilog_shortreal ||
-    dest_type.id() == ID_verilog_realtime || src_type.id() == ID_floatbv)
+    dest_type.id() == ID_verilog_realtime)
   {
-    // This may require rounding, hence add rounding mode.
-    // 1800-2017 6.12.2 requires rounding away from zero,
-    // which we don't have.
+    // The standard does not say how to round double precision
+    // to single precision floating-point.  It does not say how
+    // to round integers to float.  We simply use RNA,
+    // given the explicit requirement to use RNA when converting
+    // float to integer.
     expr.type() = verilog_lowering(dest_type);
     auto new_cast = floatbv_typecast_exprt{
       expr.op(),
       ieee_floatt::rounding_mode_expr(
-        ieee_floatt::rounding_modet::ROUND_TO_EVEN),
+        ieee_floatt::rounding_modet::ROUND_TO_AWAY),
       verilog_lowering(dest_type)};
     return std::move(new_cast);
   }