SystemVerilog: --initial-zero

The SystemVerilog standard specifies that variables are to be zero
initialized before simulation begins.  Some synthesis tools generate logic
to achieve this, whereas others do not.

This adds the option --initial-zero to match the synthesis semantics when
appropriate.

Author: kroening

CHANGELOG

@@ -1,5 +1,6 @@
 # EBMC 5.7
 
+* Verilog: --initial-zero changes the default value from nondet to zero
 * Verilog: `elsif preprocessor directive
 * Verilog: fix for named generate blocks
 * Verilog: $onehot and $onehot0 are now elaboration-time constant

regression/verilog/initial/initial-zero1.desc

@@ -0,0 +1,9 @@
+CORE
+initial-zero1.sv
+--top main --initial-zero --bound 3
+^\[main\.p1\] main\.t == 0: PROVED up to bound 3$
+^\[main\.p2\] ##1 main\.t == 5: PROVED up to bound 3$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/initial/initial-zero1.sv

@@ -0,0 +1,13 @@
+module main(input clk);
+
+  reg [7:0] t;
+
+  always_ff @(posedge clk) t = 5;
+
+  initial p1: assert property (t == 0);
+  initial p2: assert property (##1 t == 5);
+
+  chandle ch;
+  initial p3: assert property (ch == null);
+
+endmodule

src/ebmc/ebmc_parse_options.cpp

@@ -438,6 +438,7 @@ void ebmc_parse_optionst::help()
     " {y--systemverilog}             \t force SystemVerilog instead of Verilog\n"
     " {y--reset} {uexpr}             \t set up module reset\n"
     " {y--ignore-initial}            \t disregard initial blocks\n"
+    " {y--initial-zero}              \t initialize variables with zero\n"
     "\n"
     "Debugging options:\n"
     " {y--preprocess}                \t output the preprocessed source file\n"

src/ebmc/ebmc_parse_options.h

@@ -35,7 +35,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(outfile):(xml-ui)(verbosity):(gui)"
         "(json-modules):(json-properties):(json-result):"
         "(neural-liveness)(neural-engine):"
-        "(reset):(ignore-initial)"
+        "(reset):(ignore-initial)(initial-zero)"
         "(version)(verilog-rtl)(verilog-netlist)"
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"
         "(ic3)(property):(constr)(h)(new-mode)(aiger)"

src/ebmc/transition_system.cpp

@@ -178,6 +178,10 @@ static bool parse(
   if(cmdline.isset("ignore-initial"))
     options.set_option("ignore-initial", true);
 
+  // do --initial-zero
+  if(cmdline.isset("initial-zero"))
+    options.set_option("initial-zero", true);
+
   language.set_language_options(options, message_handler);
 
   message.status() << "Parsing " << filename << messaget::eom;

src/verilog/Makefile

@@ -7,6 +7,7 @@ SRC = aval_bval_encoding.cpp \
       verilog_elaborate_type.cpp \
       verilog_expr.cpp \
       verilog_generate.cpp \
+      verilog_initializer.cpp \
       verilog_interfaces.cpp \
       verilog_interpreter.cpp \
       verilog_language.cpp \

src/verilog/verilog_expr.h

@@ -1080,6 +1080,12 @@ class verilog_initialt:public verilog_statementt
     operands().resize(1);
   }
 
+  explicit verilog_initialt(verilog_statementt _statement)
+    : verilog_statementt(ID_initial)
+  {
+    add_to_operands(std::move(_statement));
+  }
+
   verilog_statementt &statement()
   {
     return static_cast<verilog_statementt &>(op0());

src/verilog/verilog_initializer.cpp

@@ -0,0 +1,49 @@
+/*******************************************************************\
+
+Module: Verilog Initializer
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "verilog_initializer.h"
+
+#include <util/arith_tools.h>
+#include <util/std_expr.h>
+
+std::optional<exprt> verilog_default_initializer(const typet &type)
+{
+  if(type.id() == ID_signedbv || type.id() == ID_unsignedbv)
+    return from_integer(0, type);
+  else if(type.id() == ID_bool)
+    return false_exprt{};
+  else if(type.id() == ID_array)
+  {
+    auto &array_type = to_array_type(type);
+    auto default_element_opt =
+      verilog_default_initializer(array_type.element_type());
+    if(!default_element_opt.has_value())
+      return {};
+    else
+      return array_of_exprt{*default_element_opt, array_type};
+  }
+  else if(type.id() == ID_struct)
+  {
+    auto &struct_type = to_struct_type(type);
+    exprt::operandst member_values;
+    for(auto &component : struct_type.components())
+    {
+      auto member_value_opt = verilog_default_initializer(component.type());
+      if(!member_value_opt.has_value())
+        return {};
+      member_values.push_back(*member_value_opt);
+    }
+    return struct_exprt{std::move(member_values), struct_type};
+  }
+  else if(type.id() == ID_verilog_chandle)
+  {
+    return constant_exprt{ID_NULL, type};
+  }
+  else
+    return {};
+}

src/verilog/verilog_initializer.h

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Verilog Initializer
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_VERILOG_INITIALIZER_H
+#define CPROVER_VERILOG_INITIALIZER_H
+
+#include <optional>
+
+class exprt;
+class typet;
+
+/// The default initial value, 1800-2017 Table 6-7
+std::optional<exprt> verilog_default_initializer(const typet &);
+
+#endif