Verilog: simulation time system functions

[kroening]

This adds support for the simulation time system functions of IEEE
1800-2017 clause 20.3, i.e., $time, $stime and $realtime.

Root cause

These three functions were simply absent from the system function
dispatch in verilog_typecheck_exprt::convert_system_function, and hence
the final else branch rejected them with

unknown system function `$realtime'

There was no synthesis support for them either.

Semantics

The result types follow 1800-2017 20.3:

• $time (20.3.1) is a 64-bit integer,
• $stime (20.3.3) is the low-order 32 bits thereof, i.e., a 32-bit
  unsigned integer,
• $realtime (20.3.2) is a real. Note that 1800-2017 6.12.1 makes
  realtime a synonym of real.

EBMC has no notion of continuous simulation time: there is no event
queue, delay controls are ignored, and `timescale/timeunit are
not taken into account. The model of time is the sequence of timeframes
of the transition system. We therefore let the time advance by exactly
one time unit per timeframe, and model the simulation time using a
global state variable $root.$time of type unsignedbv[64] that is
created on first use, with

init:  $time == 0
trans: next($time) == $time + 1

$time reads that variable, $stime is a truncating cast to 32 bits
(which is exactly the "low-order 32 bits" of 20.3.3), and $realtime
is a conversion to floatbv using the same rounding mode as the
lowering of integer-to-real casts.

Using an ordinary state variable rather than a new IR node means that no
backend changes are required: this works for word-level BMC, the
bit-level/AIG engine, BDDs, k-induction, IC3 and new-IC3, as well as for
the --smv-word-level, --verilog-rtl and --show-trans output
backends. This was checked for each of these engines.

Limitations

• One time unit per timeframe; `timescale, timeunit and #delay
  are ignored, and hence absolute times will not agree with an
  event-driven simulator when these are used.
• The simulation time is global, and is not scaled to the time unit of
  the invoking module.
• $time is given the two-valued type unsignedbv[64] rather than the
  four-valued time type, as the value is always known.
• $bits($realtime) still fails, as $bits does not support real;
  this is pre-existing and independent of this change.
• Comparing a real-typed variable in a property still trips an
  invariant in boolbv_equality; this too is pre-existing (it reproduces
  without $realtime) and is not addressed here.

Tests

This fixes the KNOWNBUG test added in #2087, which is turned into a
CORE test, and adds tests time1, stime1 and realtime2 covering
the value of the time in successive timeframes, the widths of the
results, and a refuted property.