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,10 @@
+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);
+
+endmodule

src/ebmc/ebmc_parse_options.cpp

@@ -401,6 +401,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_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
   {