Verilog: conversion for real literals

This adds conversion for real-typed literals, represented as IEEE double
precision.

regression/verilog/expressions/real-index.sv

@@ -2,6 +2,6 @@ module main;
 
   // 1800-2017 6.12.1
   reg [7:0] vector;
-  wire x = vector[real'(1.5)];
+  wire x = vector[1.5];
 
 endmodule

src/verilog/expr2verilog.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
+#include <util/ieee_float.h>
 #include <util/lispexpr.h>
 #include <util/lispirep.h>
 #include <util/namespace.h>
@@ -1120,6 +1121,14 @@ expr2verilogt::resultt expr2verilogt::convert_constant(
     const irep_idt &value = src.get_value();
     dest=id2string(value);
   }
+  else if(type.id() == ID_verilog_real)
+  {
+    constant_exprt tmp = src;
+    tmp.type() = ieee_float_spect::double_precision().to_type();
+    ieee_floatt ieee_float;
+    ieee_float.from_expr(src);
+    return {precedence, ieee_float.to_ansi_c_string()};
+  }
   else
     return convert_norep(src, precedence);
 

src/verilog/verilog_typecheck_expr.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/bitvector_expr.h>
 #include <util/ebmc_util.h>
 #include <util/expr_util.h>
+#include <util/ieee_float.h>
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/namespace.h>
@@ -1276,6 +1277,77 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
   }
 
   // check representation
+  if(rest.find('.') != std::string::npos || rest.find('e') != std::string::npos) // real?
+  {
+    const char *p=rest.c_str();
+
+    std::string str_whole_number,
+                str_fraction_part,
+                str_exponent;
+
+    // get whole number part
+    while(*p!='.' && *p!=0 && *p!='e')
+    {
+      str_whole_number+=*p;
+      p++;
+    }
+
+    // skip dot
+    if(*p=='.')
+      p++;
+
+    // get fraction part
+    while(*p != 0 && *p != 'e')
+    {
+      str_fraction_part+=*p;
+      p++;
+    }
+
+    // skip e
+    if(*p=='e')
+      p++;
+
+    // skip +
+    if(*p=='+')
+      p++;
+
+    // get exponent
+    while(*p != 0)
+    {
+      str_exponent+=*p;
+      p++;
+    }
+
+    std::string str_number=str_whole_number+
+                           str_fraction_part;
+
+    mp_integer significand;
+
+    if(str_number.empty())
+      significand=0;
+    else
+      significand=string2integer(str_number, 10);
+
+    mp_integer exponent;
+
+    if(str_exponent.empty())
+      exponent=0;
+    else
+      exponent=string2integer(str_exponent, 10);
+
+    // adjust exponent
+    exponent-=str_fraction_part.size();
+
+    ieee_floatt ieee_float{ieee_float_spect::double_precision()};
+
+    ieee_float.from_base10(significand, exponent);
+
+    constant_exprt result = ieee_float.to_expr();
+    result.type() = verilog_real_typet{};
+    result.add_source_location() = expr.source_location();
+
+    return std::move(result);
+  }
 
   std::string::size_type pos=rest.find('\'');
   std::size_t bits = 0;