Merge pull request #1428 from diffblue/verilog-parameter-port-declarations

Verilog: parameter port declarations

Author: tautschnig

src/hw_cbmc_irep_ids.h

@@ -311,11 +311,11 @@ IREP_ID_ONE(verilog_module)
 IREP_ID_ONE(verilog_package)
 IREP_ID_ONE(verilog_package_import)
 IREP_ID_ONE(verilog_package_scope)
+IREP_ID_ONE(verilog_parameter_port_decls)
 IREP_ID_ONE(verilog_program)
 IREP_ID_ONE(verilog_udp)
 IREP_ID_ONE(module_source)
 IREP_ID_ONE(module_items)
-IREP_ID_ONE(parameter_port_list)
 IREP_ID_ONE(named_block)
 IREP_ID_ONE(primitive_module_instance)
 IREP_ID_ONE(all)

src/verilog/parser.y

@@ -1984,12 +1984,13 @@ list_of_variable_identifiers:
 // to cover list_of_param_assignments.
 parameter_port_declaration:
           TOK_PARAMETER data_type_or_implicit param_assignment
-		{ $$ = $3; }
+		{ init($$, ID_decl); stack_expr($$).type() = std::move(stack_type($2)); mto($$, $3); }
 	| TOK_LOCALPARAM data_type_or_implicit param_assignment
-		{ $$ = $3; }
+		{ init($$, ID_decl); stack_expr($$).type() = std::move(stack_type($2)); mto($$, $3); }
 	| data_type param_assignment
-		{ $$ = $2; }
+		{ init($$, ID_decl); stack_expr($$).type() = std::move(stack_type($1)); mto($$, $2); }
 	| param_assignment
+		{ init($$, ID_decl); mto($$, $1); }
 	;
 
 list_of_defparam_assignments:

src/verilog/verilog_elaborate.cpp

@@ -987,8 +987,9 @@ verilog_typecheckt::elaborate(const verilog_module_sourcet &module_source)
   // and the expansion of generate blocks.
 
   // At the top level of the module, include the parameter ports.
-  for(auto &parameter_port_decl : module_source.parameter_port_list())
-    collect_symbols(typet(ID_nil), parameter_port_decl);
+  for(auto &declaration : module_source.parameter_port_decls())
+    for(auto &declarator : declaration.declarators())
+      collect_symbols(typet(ID_nil), declarator);
 
   // At the top level of the module, include the non-parameter module port
   // module items.

src/verilog/verilog_expr.cpp

@@ -61,9 +61,9 @@ void verilog_module_sourcet::show(std::ostream &out) const
 {
   out << "Module: " << base_name() << '\n';
 
-  out << "  Parameters:\n";
+  out << "  Parameter ports:\n";
 
-  for(auto &parameter : parameter_port_list())
+  for(auto &parameter : parameter_port_decls())
     out << "    " << parameter.pretty() << '\n';
 
   out << '\n';

src/verilog/verilog_expr.h

@@ -2355,17 +2355,18 @@ class verilog_module_sourcet : public verilog_item_containert
   {
   }
 
-  using parameter_port_listt = verilog_parameter_declt::declaratorst;
+  using parameter_port_declst = std::vector<verilog_parameter_declt>;
 
-  const parameter_port_listt &parameter_port_list() const
+  const parameter_port_declst &parameter_port_decls() const
   {
-    return (
-      const parameter_port_listt &)(find(ID_parameter_port_list).get_sub());
+    return (const parameter_port_declst &)(find(ID_verilog_parameter_port_decls)
+                                             .get_sub());
   }
 
-  parameter_port_listt &parameter_port_list()
+  parameter_port_declst &parameter_port_decls()
   {
-    return (parameter_port_listt &)(add(ID_parameter_port_list).get_sub());
+    return (
+      parameter_port_declst &)(add(ID_verilog_parameter_port_decls).get_sub());
   }
 
   using port_listt = std::vector<verilog_declt>;

src/verilog/verilog_parameterize_module.cpp

@@ -33,10 +33,11 @@ verilog_typecheckt::get_parameter_declarators(
   std::vector<verilog_parameter_declt::declaratort> declarators;
 
   // We do the parameter ports first.
-  const auto &parameter_port_list = module_source.parameter_port_list();
+  const auto &parameter_port_decls = module_source.parameter_port_decls();
 
-  for(auto &decl : parameter_port_list)
-    declarators.push_back(decl);
+  for(auto &declaration : parameter_port_decls)
+    for(auto &declarator : declaration.declarators())
+      declarators.push_back(declarator);
 
   // We do the module item ports second.
   const auto &module_items = module_source.module_items();
@@ -155,18 +156,20 @@ void verilog_typecheckt::set_parameter_values(
 {
   auto p_it=parameter_values.begin();
 
-  auto &parameter_port_list = module_source.parameter_port_list();
+  auto &parameter_port_decls = module_source.parameter_port_decls();
 
-  for(auto &declarator : parameter_port_list)
-  {
-    DATA_INVARIANT(p_it != parameter_values.end(), "have enough parameter values");
+  for(auto &declaration : parameter_port_decls)
+    for(auto &declarator : declaration.declarators())
+    {
+      DATA_INVARIANT(
+        p_it != parameter_values.end(), "have enough parameter values");
 
-    // only overwrite when actually assigned
-    if(p_it->is_not_nil())
-      declarator.value() = *p_it;
+      // only overwrite when actually assigned
+      if(p_it->is_not_nil())
+        declarator.value() = *p_it;
 
-    p_it++;
-  }
+      p_it++;
+    }
 
   auto &module_items = module_source.module_items();
 

src/verilog/verilog_parse_tree.cpp

@@ -25,7 +25,7 @@ exprt verilog_parse_treet::create_module(
   irept &attributes,
   irept &module_keyword,
   exprt &name,
-  exprt &parameter_port_list,
+  exprt &parameter_port_decls,
   exprt &ports,
   exprt &module_items)
 {
@@ -35,7 +35,8 @@ exprt verilog_parse_treet::create_module(
 
   verilog_module_sourcet new_module{name.id()};
 
-  new_module.add(ID_parameter_port_list) = std::move(parameter_port_list);
+  new_module.add(ID_verilog_parameter_port_decls) =
+    std::move(parameter_port_decls);
   new_module.add(ID_ports) = std::move(ports);
   new_module.add_source_location() =
     ((const exprt &)module_keyword).source_location();