From 534bf9ef65e2856c314644d97d267512868d707a Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 3 Oct 2024 18:23:53 -0700
Subject: [PATCH] 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.
---
 regression/verilog/nets/implicit5.desc |  6 ++---
 src/verilog/verilog_typecheck_expr.cpp | 32 +++++++++++++++-----------
 src/verilog/verilog_typecheck_expr.h   |  3 ++-
 3 files changed, 24 insertions(+), 17 deletions(-)

diff --git a/regression/verilog/nets/implicit5.desc b/regression/verilog/nets/implicit5.desc
index 2222bba7..c1b43288 100644
--- a/regression/verilog/nets/implicit5.desc
+++ b/regression/verilog/nets/implicit5.desc
@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 implicit5.sv
 --bound 0
-^EXIT=0$
+^file .* line 4: unknown identifier O$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This case should be errored.
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index aec7705b..f8c4aa5b 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -898,7 +898,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)
   {
@@ -936,7 +936,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();
 
@@ -1023,19 +1025,23 @@ 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);
+
+      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;
+    }
   }
 }
 
diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h
index 7f965131..577467c0 100644
--- a/src/verilog/verilog_typecheck_expr.h
+++ b/src/verilog/verilog_typecheck_expr.h
@@ -158,7 +158,8 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 private:
   [[nodiscard]] exprt convert_expr_rec(exprt expr);
   [[nodiscard]] exprt convert_constant(constant_exprt);
-  [[nodiscard]] exprt convert_symbol(symbol_exprt);
+  [[nodiscard]] exprt
+  convert_symbol(symbol_exprt, const std::optional<typet> &implicit_net_type);
   [[nodiscard]] exprt
     convert_hierarchical_identifier(class hierarchical_identifier_exprt);
   [[nodiscard]] exprt convert_nullary_expr(nullary_exprt);