Merge pull request #891 from diffblue/floatbv-typecast

Verilog: add rounding mode to casts to real/shortreal

Author: tautschnig

regression/verilog/expressions/cast_to_real1.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+cast_to_real1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/expressions/cast_to_real1.sv

@@ -0,0 +1,11 @@
+module main;
+
+  // no rounding
+  p0: assert final (real'(0) == 0.0);
+  p1: assert final (real'(1) == 1.0);
+
+  // rounding
+  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

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

regression/verilog/expressions/cast_to_real2.sv

@@ -0,0 +1,5 @@
+module main;
+
+  p0: assert final (real'(-1) == -1.0);
+
+endmodule

regression/verilog/expressions/cast_to_real3.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+cast_to_real3.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The flattening solver fails with a width error.

regression/verilog/expressions/cast_to_real3.sv

@@ -0,0 +1,5 @@
+module main;
+
+  p0: assert final (real'(1'b1) == 1);
+
+endmodule

src/verilog/verilog_lowering.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/c_types.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 
 #include "aval_bval_encoding.h"
@@ -272,7 +273,18 @@ exprt verilog_lowering(exprt expr)
       }
     }
 
-    return expr;
+    // Cast to float? Turn into floatbv_typecast,
+    // with rounding mode.
+    if(typecast_expr.type().id() == ID_floatbv)
+    {
+      auto rm = ieee_floatt::rounding_mode_expr(
+        ieee_floatt::rounding_modet::ROUND_TO_EVEN);
+      auto floatbv_typecast =
+        floatbv_typecast_exprt{typecast_expr.op(), rm, typecast_expr.type()};
+      return std::move(floatbv_typecast);
+    }
+    else
+      return expr;
   }
   else if(expr.id() == ID_verilog_explicit_type_cast)
   {