SystemVerilog: --initial-zero

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);