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

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

@@ -417,6 +417,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

@@ -1073,6 +1073,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,48 @@
+/*******************************************************************\
+
+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_zero_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 zero_element_opt = verilog_zero_initializer(array_type.element_type());
+    if(!zero_element_opt.has_value())
+      return {};
+    else
+      return array_of_exprt{*zero_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_zero_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,19 @@
+/*******************************************************************\
+
+Module: Verilog Initializer
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_VERILOG_INITIALIZER_H
+#define CPROVER_VERILOG_INITIALIZER_H
+
+#include <optional>
+
+class exprt;
+class typet;
+
+std::optional<exprt> verilog_zero_initializer(const typet &);
+
+#endif

src/verilog/verilog_language.cpp

@@ -40,6 +40,7 @@ void verilog_languaget::set_language_options(
   initial_defines = options.get_list_option("defines");
   warn_implicit_nets = options.get_bool_option("warn-implicit-nets");
   ignore_initial = options.get_bool_option("ignore-initial");
+  initial_zero = options.get_bool_option("initial-zero");
 }
 
 /*******************************************************************\
@@ -196,6 +197,7 @@ bool verilog_languaget::typecheck(
        module,
        parse_tree.standard,
        ignore_initial,
+       initial_zero,
        message_handler))
   {
     return true;

src/verilog/verilog_language.h

@@ -95,6 +95,7 @@ class verilog_languaget:public languaget
   bool vl2smv_extensions = false;
   bool warn_implicit_nets = false;
   bool ignore_initial = false;
+  bool initial_zero = false;
   std::list<std::string> include_paths;
   std::list<std::string> initial_defines;
   verilog_parse_treet parse_tree;

src/verilog/verilog_synthesis.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include "expr2verilog.h"
 #include "sva_expr.h"
 #include "verilog_expr.h"
+#include "verilog_initializer.h"
 #include "verilog_lowering.h"
 #include "verilog_typecheck_expr.h"
 
@@ -1463,6 +1464,7 @@ void verilog_synthesist::synth_module_instance(
     module_identifier,
     standard,
     ignore_initial,
+    initial_zero,
     get_message_handler());
 
   for(auto &instance : statement.instances())
@@ -1933,6 +1935,8 @@ void verilog_synthesist::synth_decl(const verilog_declt &statement) {
   {
     DATA_INVARIANT(declarator.id() == ID_declarator, "must have declarator");
 
+    auto lhs = declarator.symbol_expr();
+
     // This is reg x = ... or wire x = ...
     if(declarator.has_value())
     {
@@ -1941,9 +1945,7 @@ void verilog_synthesist::synth_decl(const verilog_declt &statement) {
       construct=constructt::INITIAL;
       event_guard=event_guardt::NONE;
 
-      auto lhs = declarator.symbol_expr();
       auto rhs = declarator.value();
-
       const symbolt &symbol = ns.lookup(lhs);
 
       if(symbol.is_state_var)
@@ -1964,6 +1966,26 @@ void verilog_synthesist::synth_decl(const verilog_declt &statement) {
         synth_continuous_assign(assign);
       }
     }
+    else if(initial_zero)
+    {
+      const symbolt &symbol = ns.lookup(lhs);
+
+      if(symbol.is_state_var)
+      {
+        // much like: initial LHS=0;
+        auto rhs_opt = verilog_zero_initializer(lhs.type());
+        if(!rhs_opt.has_value())
+        {
+          throw errort().with_location(declarator.source_location())
+            << "cannot zero-initialize `" << to_string(lhs) << "'";
+        }
+        verilog_initialt initial{verilog_blocking_assignt{lhs, *rhs_opt}};
+        initial.statement().add_source_location() =
+          declarator.source_location();
+        initial.add_source_location() = declarator.source_location();
+        synth_initial(initial);
+      }
+    }
   }
 }
 
@@ -3724,11 +3746,18 @@ bool verilog_synthesis(
   const irep_idt &module,
   verilog_standardt standard,
   bool ignore_initial,
+  bool initial_zero,
   message_handlert &message_handler)
 {
   const namespacet ns(symbol_table);
   verilog_synthesist verilog_synthesis(
-    standard, ignore_initial, ns, symbol_table, module, message_handler);
+    standard,
+    ignore_initial,
+    initial_zero,
+    ns,
+    symbol_table,
+    module,
+    message_handler);
   return verilog_synthesis.typecheck_main();
 }
 
@@ -3757,7 +3786,13 @@ bool verilog_synthesis(
     message_handler.get_message_count(messaget::M_ERROR);
 
   verilog_synthesist verilog_synthesis(
-    standard, false, ns, symbol_table, module_identifier, message_handler);
+    standard,
+    false,
+    false,
+    ns,
+    symbol_table,
+    module_identifier,
+    message_handler);
 
   try
   {

src/verilog/verilog_synthesis.h

@@ -20,6 +20,7 @@ bool verilog_synthesis(
   const irep_idt &module,
   verilog_standardt,
   bool ignore_initial,
+  bool initial_zero,
   message_handlert &);
 
 bool verilog_synthesis(

src/verilog/verilog_synthesis_class.h

@@ -43,13 +43,15 @@ class verilog_synthesist:
   verilog_synthesist(
     verilog_standardt _standard,
     bool _ignore_initial,
+    bool _initial_zero,
     const namespacet &_ns,
     symbol_table_baset &_symbol_table,
     const irep_idt &_module,
     message_handlert &_message_handler)
     : verilog_typecheck_baset(_standard, _ns, _message_handler),
       verilog_symbol_tablet(_symbol_table),
       ignore_initial(_ignore_initial),
+      initial_zero(_initial_zero),
       value_map(NULL),
       module(_module),
       temporary_counter(0)
@@ -70,6 +72,7 @@ class verilog_synthesist:
 
 protected:
   bool ignore_initial;
+  bool initial_zero;
 
   [[nodiscard]] exprt synth_expr_rec(exprt expr, symbol_statet symbol_state);