Merge pull request #1258 from diffblue/port_with_value1-fix

Verilog: module port declarations with default value

Author: tautschnig

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

@@ -1,7 +1,9 @@
-KNOWNBUG
+CORE
 port_with_value1.sv
 
-^EXIT=0$
+^\[main\.m1\.eq] always M1\.in1 == M1\.in2: REFUTED$
+^\[main\.m2\.eq] always M1\.in1 == M1\.in2: PROVED .*$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/modules/port_with_value1.sv

@@ -1,14 +1,14 @@
 module M1(input [31:0] in1 = 1234, in2 = 4567);
 
-  assert final (in1 == in2);
+  eq: assert final (in1 == in2);
 
 endmodule
 
 module main;
-  // inputs not connected
+  // inputs not connected, should fail
   M1 m1();
 
-  // in2 connected
+  // 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

@@ -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,
+              port_symbol.value,
+              replace_map,
+              inst.source_location(),
+              trans);
+        }
+      }
   }
   else // just a list without names
   {