Merge pull request #1513 from diffblue/implicit_declaration1-fix

Bugfix: type of implicit nets

Author: tautschnig

CHANGELOG

@@ -2,6 +2,7 @@
 
 * Verilog: fix for four-valued | and &
 * Verilog: fix for typed parameter ports
+* Verilog: fix for the type of implicit nets for continous assignments
 * SystemVerilog: fix for type parameters
 * SystemVerilog: type parameter ports
 * SMV: word constants

regression/verilog/assignments/implicit_declaration1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 implicit_declaration1.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This gives the wrong answer.

regression/verilog/nets/implicit4.sv

@@ -5,7 +5,7 @@ module main;
   // implicit nets are allowed on the LHS of a continuous assignment
   assign O = A & B;
 
-  always assert final (O == (A & B));
-  always assert final ($bits(O) == 4);
+  always assert final (O == (A & B & 1'b1));
+  always assert final ($bits(O) == 1);
 
 endmodule

src/verilog/verilog_typecheck.cpp

@@ -857,16 +857,18 @@ void verilog_typecheckt::convert_continuous_assign(
     exprt &rhs = to_binary_expr(*it).rhs();
 
     // 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);
-
+    // used as the LHS of a continuous assignment. The type is _not_
+    // derived from the RHS, but instead a "scalar net of default net type".
     if(lhs.id() == ID_verilog_identifier)
-      lhs =
-        convert_verilog_identifier(to_verilog_identifier_expr(lhs), rhs.type());
+    {
+      lhs = convert_verilog_identifier(
+        to_verilog_identifier_expr(lhs), unsignedbv_typet{1});
+    }
     else
       convert_expr(lhs);
 
+    convert_expr(rhs);
+
     assignment_conversion(rhs, lhs.type());
 
     check_lhs(lhs, A_CONTINUOUS);