Merge pull request #824 from diffblue/verilog-real-literals

Verilog: conversion for real literals

Author: tautschnig

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

regression/verilog/system-functions/typename1.sv

@@ -9,6 +9,9 @@ module main;
   assert final ($typename(vector1)=="bit[31:0]");
   assert final ($typename(vector2)=="bit[0:31]");
   assert final ($typename(vector3)=="bit signed[31:0]");
+  assert final ($typename(real'(1))=="real");
+  assert final ($typename(shortreal'(1))=="shortreal");
+  assert final ($typename(realtime'(1))=="realtime");
 
   // $typename yields an elaboration-time constant
   parameter P = $typename(some_bit);

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(tmp);
+    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>
@@ -694,6 +695,18 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
   {
     s = "bit signed[" + to_string(left) + ":" + to_string(right) + "]";
   }
+  else if(type.id() == ID_verilog_realtime)
+  {
+    s = "realtime";
+  }
+  else if(type.id() == ID_verilog_real)
+  {
+    s = "real";
+  }
+  else if(type.id() == ID_verilog_shortreal)
+  {
+    s = "shortreal";
+  }
   else
     s = "?";
 
@@ -1276,6 +1289,77 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
   }
 
   // check representation
+  if(
+    rest.find('.') != std::string::npos ||
+    (rest.find('h') == 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;
@@ -2104,7 +2188,10 @@ void verilog_typecheck_exprt::implicit_typecast(
       expr = typecast_exprt{expr, dest_type};
       return;
     }
-    else if(dest_type.id()==ID_verilog_realtime)
+    else if(
+      dest_type.id() == ID_verilog_realtime ||
+      dest_type.id() == ID_verilog_real ||
+      dest_type.id() == ID_verilog_shortreal)
     {
       expr = typecast_exprt{expr, dest_type};
       return;
@@ -2188,6 +2275,14 @@ void verilog_typecheck_exprt::implicit_typecast(
         << '\'';
     }
   }
+  else if(src_type.id() == ID_verilog_real)
+  {
+    if(dest_type.id() == ID_verilog_realtime)
+    {
+      expr = typecast_exprt{expr, dest_type};
+      return;
+    }
+  }
 
   throw errort().with_location(expr.source_location())
     << "failed to convert `" << to_string(src_type) << "' to `"
@@ -2453,9 +2548,9 @@ typet verilog_typecheck_exprt::max_type(
     return t0;
 
   // If one of the operands is a real, we return the real.
-  if(vt0.is_verilog_realtime())
+  if(vt0.is_verilog_real())
     return t0;
-  else if(vt1.is_verilog_realtime())
+  else if(vt1.is_verilog_real())
     return t1;
 
   bool is_verilogbv=

src/verilog/vtype.cpp

@@ -63,10 +63,15 @@ vtypet::vtypet(const typet &type)
     vtype=VERILOG_UNSIGNED;
     width=to_verilog_unsignedbv_type(type).get_width();
   }
-  else if(type.id()==ID_verilog_realtime)
+  else if(type.id() == ID_verilog_realtime || type.id() == ID_verilog_real)
   {
-    vtype=VERILOG_REALTIME;
-    width=0;
+    vtype = VERILOG_REAL;
+    width = 64;
+  }
+  else if(type.id() == ID_verilog_shortreal)
+  {
+    vtype = VERILOG_REAL;
+    width = 32;
   }
   else 
   {
@@ -109,8 +114,8 @@ std::ostream &operator << (std::ostream &out, const vtypet &vtype)
   case vtypet::BOOL:
     return out << "bool";
 
-  case vtypet::VERILOG_REALTIME:
-    return out << "bool";
+  case vtypet::VERILOG_REAL:
+    return out << "real";
 
   case vtypet::UNKNOWN:
   case vtypet::OTHER:

src/verilog/vtype.h

@@ -27,13 +27,25 @@ class vtypet
   inline bool is_integer() const { return vtype==INTEGER; }
   inline bool is_verilog_signed() const { return vtype==VERILOG_SIGNED; }
   inline bool is_verilog_unsigned() const { return vtype==VERILOG_UNSIGNED; }
-  inline bool is_verilog_realtime() const { return vtype==VERILOG_REALTIME; }
+  inline bool is_verilog_real() const
+  {
+    return vtype == VERILOG_REAL;
+  }
   inline bool is_other() const { return vtype==OTHER; }
 
 protected:
-  typedef enum { UNKNOWN, BOOL, SIGNED, UNSIGNED, INTEGER,
-                 VERILOG_SIGNED, VERILOG_UNSIGNED, 
-                 VERILOG_REALTIME, OTHER } _vtypet;
+  typedef enum
+  {
+    UNKNOWN,
+    BOOL,
+    SIGNED,
+    UNSIGNED,
+    INTEGER,
+    VERILOG_SIGNED,
+    VERILOG_UNSIGNED,
+    VERILOG_REAL,
+    OTHER
+  } _vtypet;
   _vtypet vtype;
   unsigned width;