Merge pull request #750 from diffblue/implicit-nets-type

Verilog: set type of implicit nets

Author: kroening

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$

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.

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$

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.

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.

regression/verilog/nets/implicit6.desc

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

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

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.

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

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

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

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

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

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;

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

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

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(

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
   {