Verilog: module port declarations with default value

regression/verilog/modules/missing_connection1.desc

@@ -1,7 +1,7 @@
 CORE
 missing_connection1.v
 
-^file missing_connection1\.v line 7: wrong number of arguments: expected 2 but got 1$
+^file missing_connection1\.v line 7: wrong number of port connections: expected 2 but got 1$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/verilog/modules/port_with_value1.desc

@@ -0,0 +1,11 @@
+CORE
+port_with_value1.sv
+
+^\[main\.m1\.eq] always M1\.in1 == M1\.in2: REFUTED$
+^\[main\.m2\.eq] always M1\.in1 == M1\.in2: PROVED .*$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This yields a syntax error.

regression/verilog/modules/port_with_value1.sv

@@ -0,0 +1,14 @@
+module M1(input [31:0] in1 = 1234, in2 = 4567);
+
+  eq: assert final (in1 == in2);
+
+endmodule
+
+module main;
+  // inputs not connected, should fail
+  M1 m1();
+
+  // in2 connected, should pass
+  M1 m2(.in2(1234));
+
+endmodule

regression/verilog/modules/port_with_value2.desc

@@ -0,0 +1,9 @@
+CORE
+port_with_value2.sv
+
+^file .* line 2: output ports must not have a default value$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/modules/port_with_value2.sv

@@ -0,0 +1,4 @@
+// output ports must not have a default value
+module M(output [31:0] o = 4567);
+
+endmodule

regression/verilog/modules/port_with_value3.desc

@@ -0,0 +1,9 @@
+CORE
+port_with_value3.sv
+
+^file .* line 2: expected constant expression, but got `M\.a'$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/modules/port_with_value3.sv

@@ -0,0 +1,4 @@
+// default values for inputs must be constants
+module M(input a, input b = a);
+
+endmodule

src/verilog/parser.y

@@ -899,14 +899,15 @@ ansi_port_declaration_brace:
 
           // append to last one -- required to make 
           // the grammar LR1
-	| ansi_port_declaration_brace ',' port_identifier
+	| ansi_port_declaration_brace ',' port_identifier ansi_port_initializer_opt
 		{ $$=$1;
 		  exprt decl(ID_decl);
 		  decl.add_to_operands(std::move(stack_expr($3)));
 		  // grab the type and class from previous!
 		  const irept &prev=stack_expr($$).get_sub().back();
                   decl.set(ID_type, prev.find(ID_type));
                   decl.set(ID_class, prev.find(ID_class));
+                  decl.set(ID_value, stack_expr($4));
 		  stack_expr($$).move_to_sub(decl);
 		}
 	;
@@ -935,6 +936,7 @@ ansi_port_declaration:
                   // and the unpacked_array_type goes onto the declarator.
                   stack_expr($$).type() = std::move(stack_expr($1).type());
                   addswap($2, ID_type, $3);
+                  stack_expr($2).set(ID_value, stack_expr($4));
                   mto($$, $2); /* declarator */ }
 	| variable_port_header port_identifier unpacked_dimension_brace ansi_port_initializer_opt
 		{ init($$, ID_decl);
@@ -946,6 +948,7 @@ ansi_port_declaration:
                   // and the unpacked_array_type goes onto the declarator.
                   stack_expr($$).type() = std::move(stack_expr($1).type());
                   addswap($2, ID_type, $3);
+                  stack_expr($2).set(ID_value, stack_expr($4));
                   mto($$, $2); /* declarator */ }
 	;
 

src/verilog/verilog_elaborate.cpp

@@ -62,6 +62,21 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl)
     new_symbol.base_name = base_name;
     new_symbol.pretty_name = strip_verilog_prefix(new_symbol.name);
 
+    // When using ANSI style, input ports may have an
+    // elaboration-time constant default value
+    auto &default_value = declarator.value();
+    if(default_value.is_not_nil())
+    {
+      if(new_symbol.is_output)
+        throw errort{}.with_location(default_value.source_location())
+          << "output ports must not have a default value";
+
+      auto value = default_value;
+      convert_expr(value);
+      auto elaborated_value = elaborate_constant_expression_check(value);
+      new_symbol.value = elaborated_value;
+    }
+
     add_symbol(std::move(new_symbol));
   }
 }

src/verilog/verilog_synthesis.cpp

@@ -1409,17 +1409,17 @@ Function: verilog_synthesist::instantiate_ports
 
 void verilog_synthesist::instantiate_ports(
   const irep_idt &instance,
-  const exprt &inst,
+  const verilog_instt::instancet &inst,
   const symbolt &symbol,
   const replace_mapt &replace_map,
   transt &trans)
 {
-  if(inst.operands().size()==0)
+  if(inst.connections().empty())
     return;
 
   // named port connection?
 
-  if(to_multi_ary_expr(inst).op0().id() == ID_named_port_connection)
+  if(inst.connections().front().id() == ID_named_port_connection)
   {
     const irept::subt &ports = symbol.type.find(ID_ports).get_sub();
 
@@ -1430,47 +1430,79 @@ void verilog_synthesist::instantiate_ports(
           to_symbol_expr((const exprt &)(port)).get_identifier());
 
     // no requirement that all ports are connected
-    for(const auto &o_it : inst.operands())
+    for(const auto &connection : inst.connections())
     {
-      if(o_it.operands().size()==2)
+      auto &named_connection = to_verilog_named_port_connection(connection);
+      const auto &port = to_symbol_expr(named_connection.port());
+      const exprt &value = named_connection.value();
+
+      if(value.is_not_nil())
       {
-        const auto &op0 = to_symbol_expr(to_binary_expr(o_it).op0());
-        const exprt &op1 = to_binary_expr(o_it).op1();
+        bool is_output = output_identifiers.find(port.get_identifier()) !=
+                         output_identifiers.end();
+        instantiate_port(
+          is_output, port, value, replace_map, inst.source_location(), trans);
+      }
+    }
+
+    std::set<irep_idt> connected_ports;
+
+    for(const auto &connection : inst.connections())
+    {
+      auto &named_connection = to_verilog_named_port_connection(connection);
+      connected_ports.insert(
+        to_symbol_expr(named_connection.port()).get_identifier());
+    }
 
-        if(op1.is_not_nil())
+    // unconnected inputs may be given a default value
+    for(auto &port : ports)
+      if(port.get_bool(ID_input))
+      {
+        auto &port_symbol_expr = to_symbol_expr((const exprt &)(port));
+        auto identifier = port_symbol_expr.get_identifier();
+        if(connected_ports.find(identifier) == connected_ports.end())
         {
-          bool is_output = output_identifiers.find(op0.get_identifier()) !=
-                           output_identifiers.end();
-          instantiate_port(
-            is_output, op0, op1, replace_map, inst.source_location(), trans);
+          auto &port_symbol = ns.lookup(port_symbol_expr);
+          if(port_symbol.value.is_not_nil())
+            instantiate_port(
+              false,
+              port_symbol_expr,
+              port_symbol.value,
+              replace_map,
+              inst.source_location(),
+              trans);
         }
       }
-    }
   }
   else // just a list without names
   {
     const irept::subt &ports = symbol.type.find(ID_ports).get_sub();
 
-    if(inst.operands().size()!=ports.size())
+    if(inst.connections().size() != ports.size())
     {
       throw errort().with_location(inst.source_location())
         << "wrong number of ports: expected " << ports.size() << " but got "
-        << inst.operands().size();
+        << inst.connections().size();
     }
 
     irept::subt::const_iterator p_it=
       ports.begin();
 
-    for(const auto &o_it : inst.operands())
+    for(const auto &connection : inst.connections())
     {
-      DATA_INVARIANT(o_it.is_not_nil(), "all ports must be connected");
+      DATA_INVARIANT(connection.is_not_nil(), "all ports must be connected");
 
       auto &port = to_symbol_expr((const exprt &)(*p_it));
 
       bool is_output = port.get_bool(ID_output);
 
       instantiate_port(
-        is_output, port, o_it, replace_map, inst.source_location(), trans);
+        is_output,
+        port,
+        connection,
+        replace_map,
+        inst.source_location(),
+        trans);
       p_it++;
     }
   }

src/verilog/verilog_synthesis_class.h

@@ -316,7 +316,7 @@ class verilog_synthesist:
 
   void instantiate_ports(
     const irep_idt &instance,
-    const exprt &inst,
+    const verilog_instt::instancet &inst,
     const symbolt &,
     const replace_mapt &,
     transt &);

src/verilog/verilog_typecheck.cpp

@@ -103,28 +103,16 @@ void verilog_typecheckt::typecheck_port_connections(
 
   const irept::subt &ports=symbol.type.find(ID_ports).get_sub();
 
-  // no arguments is one argument that is nil
-  if(
-    ports.size() == 0 && inst.connections().size() == 1 &&
-    inst.connections().front().is_nil())
+  // no connection is one connection that is nil
+  if(inst.connections().size() == 1 && inst.connections().front().is_nil())
   {
     inst.connections().clear();
   }
 
-  if(inst.connections().empty())
-  {
-    if(!ports.empty())
-    {
-      throw errort().with_location(inst.source_location())
-        << "module does not have ports";
-    }
-
-    return;
-  }
-
   // named port connection?
-
-  if(inst.connections().front().id() == ID_named_port_connection)
+  if(
+    inst.connections().empty() ||
+    inst.connections().front().id() == ID_named_port_connection)
   {
     // We don't require that all ports are connected.
 
@@ -184,8 +172,8 @@ void verilog_typecheckt::typecheck_port_connections(
     if(inst.connections().size() != ports.size())
     {
       throw errort().with_location(inst.source_location())
-        << "wrong number of arguments: expected " << ports.size() << " but got "
-        << inst.connections().size();
+        << "wrong number of port connections: expected " << ports.size()
+        << " but got " << inst.connections().size();
     }
 
     irept::subt::const_iterator p_it=