diff --git a/regression/verilog/expressions/cast_to_real1.desc b/regression/verilog/expressions/cast_to_real1.desc new file mode 100644 index 00000000..935649bc --- /dev/null +++ b/regression/verilog/expressions/cast_to_real1.desc @@ -0,0 +1,9 @@ +KNOWNBUG +cast_to_real1.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Typechecking is failing. diff --git a/regression/verilog/expressions/cast_to_real1.sv b/regression/verilog/expressions/cast_to_real1.sv new file mode 100644 index 00000000..69a4ddb0 --- /dev/null +++ b/regression/verilog/expressions/cast_to_real1.sv @@ -0,0 +1,10 @@ +module main; + + p0: assert final (real'(0) == 0.0); + p1: assert final (real'(1) == 1.0); + p2: assert final (real'(-1) == -1.0); + p3: assert final (real'(1'b1) == 1); + p4: assert final (real'('hffff_ffff_ffff_ffff) == real'('h1_0000_0000_0000_0000)); + p5: assert final (real'(-'sh0_ffff_ffff_ffff_ffff) == real'(-'sh1_0000_0000_0000_0000)); + +endmodule diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp index 1631c94f..67f85b71 100644 --- a/src/verilog/verilog_lowering.cpp +++ b/src/verilog/verilog_lowering.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #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) {