Verilog: set type of implicit nets

1800 2017 6.10 allows implicit declarations of nets.  The type of these nets
is to be derived from the LHS of the assignment or the type of the port
connection.

The warning when a net is declared implicitly is dropped by default; it can
be reactivated with --warn-implicit-nets.

Author: kroening

Diff for: regression/verilog/nets/implicit1.desc

@@ -1,6 +1,6 @@
 CORE
 implicit1.sv
---bound 0
+--bound 0 --warn-implicit-nets
 ^file .* line 4: implicit wire main\.O$
 ^file .* line 4: implicit wire main\.A$
 ^file .* line 4: implicit wire main\.B$

Diff for: regression/verilog/nets/implicit2.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 implicit2.sv
---bound 0
+--bound 0 --warn-implicit-nets
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The width of the implicit net is set incorrectly.

Diff for: regression/verilog/nets/implicit3.desc

@@ -1,6 +1,6 @@
 CORE
 implicit3.sv
---bound 0
+--bound 0 --warn-implicit-nets
 ^file .* line 6: implicit wire main\.O$
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/verilog/nets/implicit4.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 implicit4.sv
---bound 0
+--bound 0 --warn-implicit-nets
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The width of the implicit net is set incorrectly.

Diff for: regression/verilog/nets/implicit5.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 implicit5.sv
---bound 0
-^EXIT=0$
+--bound 0 --warn-implicit-nets
+^file .* line 4: unknown identifier A$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This case should be errored.

Diff for: regression/verilog/nets/implicit6.desc

@@ -0,0 +1,8 @@
+CORE
+implicit6.sv
+--bound 0 --warn-implicit-nets
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

Diff for: regression/verilog/nets/implicit6.sv

@@ -0,0 +1,10 @@
+module main;
+
+  parameter P = 2;
+
+  // implicit nets are allowed in the port connection list of a module
+  and [P:0] (O, A, B);
+
+  assert final ($bits(O) == P+1);
+
+endmodule

Diff for: regression/verilog/nets/implicit7.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+implicit7.sv
+--bound 0 --warn-implicit-nets
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The implicit net is not known yet when evaluating parameters.

Diff for: regression/verilog/nets/implicit7.sv

@@ -0,0 +1,16 @@
+module main;
+
+  parameter P = 10;
+
+  // implicit nets are allowed in the port connection list of a module
+  sub #(P) my_sub(x);
+
+  // The type of the implict net could be used to define another parameter
+  parameter Q = $bits(x);
+
+  assert final (Q == P + 1);
+
+endmodule
+
+module sub #(parameter P = 1)(input [P:0] some_input);
+endmodule

Diff for: src/ebmc/ebmc_parse_options.h

@@ -47,7 +47,8 @@ class ebmc_parse_optionst:public parse_options_baset
         "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
         "(liveness-to-safety)"
-        "I:D:(preprocess)(systemverilog)(vl2smv-extensions)",
+        "I:D:(preprocess)(systemverilog)(vl2smv-extensions)"
+        "(warn-implicit-nets)",
         argc,
         argv,
         std::string("EBMC ") + EBMC_VERSION),

Diff for: src/ebmc/transition_system.cpp

@@ -112,6 +112,7 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
   optionst options;
   options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
   options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
+  options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets"));
 
   // do -D
   if(cmdline.isset('D'))
@@ -163,6 +164,7 @@ static bool parse(
   optionst options;
   options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
   options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
+  options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets"));
 
   // do -D
   if(cmdline.isset('D'))

Diff for: src/verilog/verilog_language.cpp

@@ -37,6 +37,7 @@ void verilog_languaget::set_language_options(
   force_systemverilog = options.get_bool_option("force-systemverilog");
   vl2smv_extensions = options.get_bool_option("vl2smv-extensions");
   initial_defines = options.get_list_option("defines");
+  warn_implicit_nets = options.get_bool_option("warn-implicit-nets");
 }
 
 /*******************************************************************\
@@ -180,7 +181,8 @@ bool verilog_languaget::typecheck(
 {
   if(module=="") return false;
 
-  if(verilog_typecheck(parse_tree, symbol_table, module, message_handler))
+  if(verilog_typecheck(
+       parse_tree, symbol_table, module, warn_implicit_nets, message_handler))
     return true;
 
   messaget message(message_handler);

Diff for: src/verilog/verilog_language.h

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

Diff for: src/verilog/verilog_parameterize_module.cpp

@@ -289,7 +289,7 @@ irep_idt verilog_typecheckt::parameterize_module(
   // recursive call
 
   verilog_typecheckt verilog_typecheck(
-    standard, *new_symbol, symbol_table, get_message_handler());
+    standard, false, *new_symbol, symbol_table, get_message_handler());
 
   if(verilog_typecheck.typecheck_main())
     throw 0;

Diff for: src/verilog/verilog_synthesis.cpp

@@ -663,7 +663,7 @@ exprt verilog_synthesist::expand_function_call(
     {
       // Attempt to constant fold.
       verilog_typecheck_exprt verilog_typecheck_expr(
-        standard, ns, get_message_handler());
+        standard, false, ns, get_message_handler());
       auto result =
         verilog_typecheck_expr.elaborate_constant_system_function_call(call);
       if(!result.is_constant())

Diff for: src/verilog/verilog_typecheck.cpp

@@ -56,8 +56,17 @@ void verilog_typecheckt::typecheck_port_connection(
   }
   else
   {
-    convert_expr(op);
-   
+    // IEEE 1800 2017 6.10 allows implicit declarations of nets when
+    // used in a port connection.
+    if(op.id() == ID_symbol)
+    {
+      op = convert_symbol(to_symbol_expr(op), port.type());
+    }
+    else
+    {
+      convert_expr(op);
+    }
+
     if(symbol.is_output)
       check_lhs(op, A_CONTINUOUS);
     else
@@ -229,7 +238,17 @@ void verilog_typecheckt::typecheck_builtin_port_connections(
 
   for(auto &connection : inst.connections())
   {
-    convert_expr(connection);
+    // IEEE 1800 2017 6.10 allows implicit declarations of nets when
+    // used in a port connection.
+    if(connection.id() == ID_symbol)
+    {
+      connection = convert_symbol(to_symbol_expr(connection), type);
+    }
+    else
+    {
+      convert_expr(connection);
+    }
+
     propagate_type(connection, type);
   }
 }
@@ -821,8 +840,16 @@ void verilog_typecheckt::convert_continuous_assign(
     exprt &lhs = to_binary_expr(*it).lhs();
     exprt &rhs = to_binary_expr(*it).rhs();
 
-    convert_expr(lhs);
+    // IEEE 1800 2017 6.10 allows implicit declarations of nets when
+    // used as the LHS of a continuous assignment. The type is derived
+    // from the RHS, and hence, we convert that first.
     convert_expr(rhs);
+
+    if(lhs.id() == ID_symbol)
+      lhs = convert_symbol(to_symbol_expr(lhs), rhs.type());
+    else
+      convert_expr(lhs);
+
     propagate_type(rhs, lhs.type());
 
     check_lhs(lhs, A_CONTINUOUS);
@@ -1761,7 +1788,8 @@ Function: verilog_typecheckt::implicit_wire
 
 bool verilog_typecheckt::implicit_wire(
   const irep_idt &identifier,
-  const symbolt *&symbol_ptr)
+  const symbolt *&symbol_ptr,
+  const typet &net_type)
 {
   std::string full_identifier=
     id2string(module_identifier)+"."+id2string(identifier);
@@ -1773,7 +1801,7 @@ bool verilog_typecheckt::implicit_wire(
   symbol.value.make_nil();
   symbol.base_name=identifier;
   symbol.name=full_identifier;
-  symbol.type=bool_typet(); // TODO: other types?
+  symbol.type = net_type;
   symbol.pretty_name=strip_verilog_prefix(full_identifier);
 
   symbolt *new_symbol;
@@ -1836,6 +1864,7 @@ bool verilog_typecheck(
   const verilog_parse_treet &parse_tree,
   symbol_table_baset &symbol_table,
   const std::string &module,
+  bool warn_implicit_nets,
   message_handlert &message_handler)
 {
   verilog_parse_treet::module_mapt::const_iterator it=
@@ -1851,7 +1880,11 @@ bool verilog_typecheck(
   }
 
   return verilog_typecheck(
-    symbol_table, *it->second, parse_tree.standard, message_handler);
+    symbol_table,
+    *it->second,
+    parse_tree.standard,
+    warn_implicit_nets,
+    message_handler);
 }
 
 /*******************************************************************\
@@ -1870,6 +1903,7 @@ bool verilog_typecheck(
   symbol_table_baset &symbol_table,
   const verilog_module_sourcet &verilog_module_source,
   verilog_standardt standard,
+  bool warn_implicit_nets,
   message_handlert &message_handler)
 {
   // create symbol
@@ -1898,6 +1932,7 @@ bool verilog_typecheck(
   }
 
   verilog_typecheckt verilog_typecheck(
-    standard, *new_symbol, symbol_table, message_handler);
+    standard, warn_implicit_nets, *new_symbol, symbol_table, message_handler);
+
   return verilog_typecheck.typecheck_main();
 }

Diff for: src/verilog/verilog_typecheck.h

@@ -23,12 +23,14 @@ bool verilog_typecheck(
   const verilog_parse_treet &parse_tree,
   symbol_table_baset &,
   const std::string &module,
+  bool warn_implicit_nets,
   message_handlert &message_handler);
 
 bool verilog_typecheck(
   symbol_table_baset &,
   const verilog_module_sourcet &verilog_module_source,
   verilog_standardt,
+  bool warn_implicit_nets,
   message_handlert &message_handler);
 
 bool verilog_typecheck(
@@ -57,10 +59,15 @@ class verilog_typecheckt:
 public:
   verilog_typecheckt(
     verilog_standardt _standard,
+    bool warn_implicit_nets,
     symbolt &_module_symbol,
     symbol_table_baset &_symbol_table,
     message_handlert &_message_handler)
-    : verilog_typecheck_exprt(_standard, ns, _message_handler),
+    : verilog_typecheck_exprt(
+        _standard,
+        warn_implicit_nets,
+        ns,
+        _message_handler),
       verilog_symbol_tablet(_symbol_table),
       ns(_symbol_table),
       module_symbol(_module_symbol),
@@ -204,8 +211,10 @@ class verilog_typecheckt:
   virtual void convert_statements(verilog_module_exprt &);
 
   // to be overridden
-  bool implicit_wire(const irep_idt &identifier,
-                     const symbolt *&symbol) override;
+  bool implicit_wire(
+    const irep_idt &identifier,
+    const symbolt *&,
+    const typet &) override;
 
   // generate constructs
   void elaborate_generate_assign(

Diff for: src/verilog/verilog_typecheck_expr.cpp

@@ -893,7 +893,7 @@ exprt verilog_typecheck_exprt::convert_nullary_expr(nullary_exprt expr)
   }
   else if(expr.id()==ID_symbol)
   {
-    return convert_symbol(to_symbol_expr(std::move(expr)));
+    return convert_symbol(to_symbol_expr(std::move(expr)), {});
   }
   else if(expr.id()==ID_verilog_star_event)
   {
@@ -931,7 +931,9 @@ Function: verilog_typecheck_exprt::convert_symbol
 
 \*******************************************************************/
 
-exprt verilog_typecheck_exprt::convert_symbol(symbol_exprt expr)
+exprt verilog_typecheck_exprt::convert_symbol(
+  symbol_exprt expr,
+  const std::optional<typet> &implicit_net_type)
 {
   const irep_idt &identifier = expr.get_identifier();
 
@@ -1018,19 +1020,25 @@ exprt verilog_typecheck_exprt::convert_symbol(symbol_exprt expr)
       return std::move(expr);
     }
   }
-  else if(!implicit_wire(identifier, symbol))
-  {
-    // this should become an error
-    warning().source_location=expr.source_location();
-    warning() << "implicit wire " << symbol->display_name() << eom;
-    expr.type()=symbol->type;
-    expr.set_identifier(symbol->name);
-    return std::move(expr);
-  }
   else
   {
-    throw errort().with_location(expr.source_location())
-      << "unknown identifier " << identifier;
+    if(implicit_net_type.has_value())
+    {
+      implicit_wire(identifier, symbol, implicit_net_type.value());
+      if(warn_implicit_nets)
+      {
+        warning().source_location = expr.source_location();
+        warning() << "implicit wire " << symbol->display_name() << eom;
+      }
+      expr.type() = symbol->type;
+      expr.set_identifier(symbol->name);
+      return std::move(expr);
+    }
+    else
+    {
+      throw errort().with_location(expr.source_location())
+        << "unknown identifier " << identifier;
+    }
   }
 }
 
@@ -3259,7 +3267,7 @@ bool verilog_typecheck(
     message_handler.get_message_count(messaget::M_ERROR);
 
   verilog_typecheck_exprt verilog_typecheck_expr(
-    standard, ns, module_identifier, message_handler);
+    standard, true, ns, module_identifier, message_handler);
 
   try
   {