Verilog: simulation time system functions

regression/verilog/system-functions/realtime1.desc

@@ -1,10 +1,8 @@
-KNOWNBUG
+CORE
 realtime1.sv
 
 ^no properties$
 ^EXIT=10$
 ^SIGNAL=0$
 --
---
-$realtime is not implemented, and yields "unknown system function
-`$realtime'".  The same applies to $time and $stime.
+^warning: ignoring

regression/verilog/system-functions/realtime2.desc

@@ -0,0 +1,11 @@
+CORE
+realtime2.sv
+--bound 5
+^\[main\.p0\] ##0 \$realtime\(\) == 0: PROVED up to bound 5$
+^\[main\.p1\] ##1 \$realtime\(\) == 1: PROVED up to bound 5$
+^\[main\.p2\] ##2 \$realtime\(\) == 2: PROVED up to bound 5$
+^\[main\.p3\] ##2 \$realtime\(\) > 1\.5: PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/realtime2.sv

@@ -0,0 +1,11 @@
+module main;
+
+  // 1800-2017 20.3.2: $realtime returns the current simulation time,
+  // scaled to the time unit of the module that invokes it, as a real.
+  initial p0: assert property (##0 $realtime == 0.0);
+  initial p1: assert property (##1 $realtime == 1.0);
+  initial p2: assert property (##2 $realtime == 2.0);
+
+  initial p3: assert property (##2 $realtime > 1.5);
+
+endmodule

regression/verilog/system-functions/stime1.desc

@@ -0,0 +1,12 @@
+CORE
+stime1.sv
+--bound 5
+^\[main\.p0\] ##0 \$stime\(\) == 0: PROVED up to bound 5$
+^\[main\.p1\] ##1 \$stime\(\) == 1: PROVED up to bound 5$
+^\[main\.p2\] ##2 \$stime\(\) == 2: PROVED up to bound 5$
+^\[main\.p3\] always \$bits\(\$stime\(\)\) == 32: PROVED up to bound 5$
+^\[main\.p4\] ##3 \$stime\(\) == \$time\(\): PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/stime1.sv

@@ -0,0 +1,15 @@
+module main;
+
+  // 1800-2017 20.3.3: $stime returns the low-order 32 bits of the
+  // current simulation time, as a 32-bit unsigned integer.
+  initial p0: assert property (##0 $stime == 0);
+  initial p1: assert property (##1 $stime == 1);
+  initial p2: assert property (##2 $stime == 2);
+
+  // the width of the result is 32 bits
+  p3: assert property ($bits($stime) == 32);
+
+  // $stime and $time agree while the time is small
+  initial p4: assert property (##3 $stime == $time);
+
+endmodule

regression/verilog/system-functions/time1.desc

@@ -0,0 +1,13 @@
+CORE
+time1.sv
+--bound 5
+^\[main\.p0\] ##0 \$time\(\) == 0: PROVED up to bound 5$
+^\[main\.p1\] ##1 \$time\(\) == 1: PROVED up to bound 5$
+^\[main\.p2\] ##2 \$time\(\) == 2: PROVED up to bound 5$
+^\[main\.p3\] ##3 \$time\(\) == 3: PROVED up to bound 5$
+^\[main\.p4\] always \$bits\(\$time\(\)\) == 64: PROVED up to bound 5$
+^\[main\.p5\] ##2 \$time\(\) == 0: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/time1.sv

@@ -0,0 +1,18 @@
+module main;
+
+  // 1800-2017 20.3.1: $time returns the current simulation time,
+  // scaled to the time unit of the module that invokes it, as a
+  // 64-bit integer.  EBMC's model of time is the sequence of
+  // timeframes, i.e., time advances by one time unit per timeframe.
+  initial p0: assert property (##0 $time == 0);
+  initial p1: assert property (##1 $time == 1);
+  initial p2: assert property (##2 $time == 2);
+  initial p3: assert property (##3 $time == 3);
+
+  // the width of the result is 64 bits
+  p4: assert property ($bits($time) == 64);
+
+  // this one fails, as the time advances
+  initial p5: assert property (##2 $time == 0);
+
+endmodule

src/verilog/verilog_synthesis.cpp

@@ -14,7 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/ebmc_util.h>
 #include <util/expr_util.h>
+#include <util/floatbv_expr.h>
 #include <util/identifier.h>
+#include <util/ieee_float.h>
 #include <util/mathematical_types.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
@@ -345,6 +347,59 @@ void verilog_synthesist::function_locality(const symbolt &function_symbol)
 
 /*******************************************************************\
 
+Function: verilog_synthesist::simulation_time_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Returns the state variable that models the simulation
+          time, creating it on first use.
+
+\*******************************************************************/
+
+const symbolt &verilog_synthesist::simulation_time_symbol()
+{
+  // 1800-2017 20.3 defines the simulation time system functions in terms
+  // of the simulation time that an event-driven simulator maintains.
+  // EBMC's model of time is the sequence of timeframes of the transition
+  // system: there is no continuous time, delay controls are ignored, and
+  // so is the `timescale directive.  We therefore let the time advance by
+  // exactly one time unit per timeframe, which we model using a state
+  // variable that counts the timeframes.  Note that the simulation time
+  // is global, and hence the state variable lives in $root.
+  const auto type = unsignedbv_typet{64}; // 1800-2017 20.3.1
+
+  const irep_idt identifier =
+    id2string(verilog_root_module_identifier()) + ".$time";
+
+  // Created already?
+  auto existing_symbol = symbol_table.get_writeable(identifier);
+  if(existing_symbol != nullptr)
+    return *existing_symbol;
+
+  symbolt new_symbol{identifier, type, ID_Verilog};
+  new_symbol.base_name = "$time";
+  new_symbol.pretty_name = strip_verilog_root_prefix(identifier);
+  new_symbol.module = verilog_root_module_identifier();
+  new_symbol.is_lvalue = true; // this is a state variable
+  new_symbol.value = nil_exprt();
+
+  auto insert_result = symbol_table.insert(std::move(new_symbol));
+  CHECK_RETURN(insert_result.second);
+
+  // The time starts at zero, and is incremented once per timeframe.
+  const symbol_exprt symbol_expr{identifier, type};
+  auto &assignment = assignments[identifier];
+  assignment.init.value = from_integer(0, type);
+  assignment.next.value = plus_exprt{symbol_expr, from_integer(1, type)};
+  local_symbols.insert(identifier);
+
+  return insert_result.first;
+}
+
+/*******************************************************************\
+
 Function: verilog_synthesist::expand_function_call
 
   Inputs:
@@ -427,6 +482,37 @@ exprt verilog_synthesist::expand_function_call(
       // Return 0, indicating plusarg not found.
       return from_integer(0, call.type()).with_source_location(call);
     }
+    else if(
+      base_name == "$time" || base_name == "$stime" || base_name == "$realtime")
+    {
+      // IEEE 1800-2017 section 20.3
+      // Read the state variable that counts the timeframes.
+      exprt result = simulation_time_symbol().symbol_expr();
+
+      // The type of the call is not lowered yet.
+      auto type = verilog_lowering(call.type());
+
+      if(type.id() == ID_floatbv)
+      {
+        // $realtime.  1800-2017 does not say how to round integers to
+        // floating-point; we use the same rounding mode as the lowering
+        // of integer-to-real casts.
+        result = floatbv_typecast_exprt{
+          result,
+          ieee_floatt::rounding_mode_expr(
+            ieee_floatt::rounding_modet::ROUND_TO_AWAY),
+          type};
+      }
+      else
+      {
+        // $time and $stime.  1800-2017 20.3.3 gives the low-order 32 bits
+        // of the current simulation time for $stime, which is what the
+        // truncating cast yields.
+        result = typecast_exprt::conditional_cast(result, type);
+      }
+
+      return result.with_source_location(call);
+    }
     else
     {
       // Attempt to constant fold.

src/verilog/verilog_synthesis_class.h

@@ -349,6 +349,9 @@ class verilog_synthesist:
   exprt
   expand_function_call(const class function_call_exprt &call, symbol_statet);
 
+  // For $time, $stime and $realtime
+  const symbolt &simulation_time_symbol();
+
   void instantiate_ports(
     const irep_idt &instance,
     const verilog_instt::instancet &inst,

src/verilog/verilog_typecheck_expr.cpp

@@ -1608,6 +1608,37 @@ exprt verilog_typecheck_exprt::convert_system_function(function_call_exprt expr)
 
     return std::move(expr);
   }
+  else if(
+    base_name == "$time" || base_name == "$stime" || base_name == "$realtime")
+  {
+    // IEEE 1800-2017 section 20.3, simulation time system functions
+    if(!arguments.empty())
+    {
+      throw errort().with_location(expr.source_location())
+        << base_name << " takes no arguments";
+    }
+
+    if(base_name == "$time")
+    {
+      // 1800-2017 20.3.1: $time returns the time as a 64-bit integer.
+      // The values delivered are always known, and hence we use the
+      // two-valued type.
+      expr.type() = unsignedbv_typet{64};
+    }
+    else if(base_name == "$stime")
+    {
+      // 1800-2017 20.3.3: $stime returns an unsigned integer of 32 bits.
+      expr.type() = unsignedbv_typet{32};
+    }
+    else
+    {
+      // 1800-2017 20.3.2: $realtime returns a real number.
+      // Note that 1800-2017 6.12.1 makes 'realtime' a synonym of 'real'.
+      expr.type() = verilog_real_typet{};
+    }
+
+    return std::move(expr);
+  }
   else
   {
     throw errort().with_location(expr.function().source_location())