ebmc: --ignore-initial

This adds the --igore-initial command line option to ebmc, which allows
reasoning about the transition relation only of a Verilog file.

regression/verilog/initial/ignore-initial1.desc

@@ -0,0 +1,9 @@
+CORE
+ignore-initial1.sv
+--top main --bound 1 --ignore-initial
+^\[main\.p1\] always main\.x == 20 || main\.x == 5: REFUTED$
+^\[main\.p2\] always main\.y == 30 || main\.y == 6: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/initial/ignore-initial1.sv

@@ -0,0 +1,16 @@
+module main(input clk);
+
+  reg [7:0] x, y = 30;
+
+  initial x=20;
+
+  always_ff @(posedge clk) x=5;
+  always_ff @(posedge clk) y=6;
+
+  // fails, owing to nondeterministic initial state
+  p1: assert property (x==20 || x==5);
+
+  // fails, owing to nondeterministic initial state
+  p2: assert property (y==30 || y==6);
+
+endmodule 

regression/verilog/initial1/test.desc → regression/verilog/initial/initial1.desc

@@ -1,5 +1,5 @@
 CORE
-main.v
+initial1.v
 --module main --bound 2
 ^EXIT=0$
 ^SIGNAL=0$

src/ebmc/ebmc_parse_options.cpp

@@ -356,9 +356,6 @@ void ebmc_parse_optionst::help()
     " {y--numbered-trace}            \t give a trace with identifiers numbered by timeframe\n"
     " {y--show-properties}           \t list the properties in the model\n"
     " {y--property} {uid}            \t check the property with given ID\n"
-    " {y-I} {upath}                  \t set include path\n"
-    " {y--systemverilog}             \t force SystemVerilog instead of Verilog\n"
-    " {y--reset} {uexpr}             \t set up module reset\n"
     " {y--liveness-to-safety}        \t translate liveness properties to safety properties\n"
     "\n"
     "Methods:\n"
@@ -398,6 +395,13 @@ void ebmc_parse_optionst::help()
     " {y--yices}                     \t use Yices as solver\n"
     " {y--z3}                        \t use Z3 as solver\n"
     "\n"
+    "Verilog options:\n"
+    " {y-I} {upath}                  \t set include path\n"
+    " {y-D} {uvar}[={uvalue}]        \t set preprocessor define\n"
+    " {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"
+    "\n"
     "Debugging options:\n"
     " {y--preprocess}                \t output the preprocessed source file\n"
     " {y--show-parse}                \t show parse trees\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):"
+        "(reset):(ignore-initial)"
         "(version)(verilog-rtl)(verilog-netlist)"
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"
         "(ic3)(property):(constr)(h)(new-mode)(aiger)"

src/ebmc/transition_system.cpp

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

src/verilog/verilog_language.cpp

@@ -39,6 +39,7 @@ void verilog_languaget::set_language_options(
   include_paths = options.get_list_option("I");
   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");
 }
 
 /*******************************************************************\
@@ -191,8 +192,14 @@ bool verilog_languaget::typecheck(
   message.debug() << "Synthesis " << module << messaget::eom;
 
   if(verilog_synthesis(
-       symbol_table, module, parse_tree.standard, message_handler, optionst{}))
+       symbol_table,
+       module,
+       parse_tree.standard,
+       ignore_initial,
+       message_handler))
+  {
     return true;
+  }
 
   return false;
 }

src/verilog/verilog_language.h

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

src/verilog/verilog_synthesis.cpp

@@ -1459,7 +1459,11 @@ void verilog_synthesist::synth_module_instance(
 
   // make sure the module is synthesized already
   verilog_synthesis(
-    symbol_table, module_identifier, standard, get_message_handler(), options);
+    symbol_table,
+    module_identifier,
+    standard,
+    ignore_initial,
+    get_message_handler());
 
   for(auto &instance : statement.instances())
     expand_module_instance(module_symbol, instance, trans);
@@ -1782,6 +1786,9 @@ void verilog_synthesist::synth_initial(
       << "initial module item expected to have one operand";
   }
 
+  if(ignore_initial)
+    return;
+
   construct=constructt::INITIAL;
   event_guard=event_guardt::NONE;
 
@@ -3716,12 +3723,12 @@ bool verilog_synthesis(
   symbol_table_baset &symbol_table,
   const irep_idt &module,
   verilog_standardt standard,
-  message_handlert &message_handler,
-  const optionst &options)
+  bool ignore_initial,
+  message_handlert &message_handler)
 {
   const namespacet ns(symbol_table);
   verilog_synthesist verilog_synthesis(
-    standard, ns, symbol_table, module, options, message_handler);
+    standard, ignore_initial, ns, symbol_table, module, message_handler);
   return verilog_synthesis.typecheck_main();
 }
 
@@ -3744,14 +3751,13 @@ bool verilog_synthesis(
   message_handlert &message_handler,
   const namespacet &ns)
 {
-  optionst options;
   symbol_tablet symbol_table;
 
   const auto errors_before =
     message_handler.get_message_count(messaget::M_ERROR);
 
   verilog_synthesist verilog_synthesis(
-    standard, ns, symbol_table, module_identifier, options, message_handler);
+    standard, false, ns, symbol_table, module_identifier, message_handler);
 
   try
   {

src/verilog/verilog_synthesis.h

@@ -19,8 +19,8 @@ bool verilog_synthesis(
   symbol_table_baset &,
   const irep_idt &module,
   verilog_standardt,
-  message_handlert &,
-  const optionst &);
+  bool ignore_initial,
+  message_handlert &);
 
 bool verilog_synthesis(
   exprt &,

src/verilog/verilog_synthesis_class.h

@@ -42,14 +42,14 @@ class verilog_synthesist:
 public:
   verilog_synthesist(
     verilog_standardt _standard,
+    bool _ignore_initial,
     const namespacet &_ns,
     symbol_table_baset &_symbol_table,
     const irep_idt &_module,
-    const optionst &_options,
     message_handlert &_message_handler)
     : verilog_typecheck_baset(_standard, _ns, _message_handler),
       verilog_symbol_tablet(_symbol_table),
-      options(_options),
+      ignore_initial(_ignore_initial),
       value_map(NULL),
       module(_module),
       temporary_counter(0)
@@ -69,7 +69,7 @@ class verilog_synthesist:
   [[nodiscard]] exprt synth_expr(exprt expr, symbol_statet symbol_state);
 
 protected:
-  const optionst &options;
+  bool ignore_initial;
 
   [[nodiscard]] exprt synth_expr_rec(exprt expr, symbol_statet symbol_state);