Verilog: module port declarations with default value

This fixes the grammar to allow ANSI module port declarations that have a
default value.

This adds support for module ports (ANSI and non-ANSI) that have a default
value to the type checker.

Author: kroening

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

@@ -1444,6 +1444,35 @@ void verilog_synthesist::instantiate_ports(
           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());
+    }
+
+    // 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())
+        {
+          auto &port_symbol = ns.lookup(port_symbol_expr);
+          if(port_symbol.value.is_not_nil())
+            instantiate_port(
+              false,
+              port_symbol_expr,
+              symbol.value,
+              replace_map,
+              inst.source_location(),
+              trans);
+        }
+      }
   }
   else // just a list without names
   {

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=