Verilog: parameter port declarations

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

@@ -804,15 +804,15 @@ void verilog_typecheckt::collect_symbols(
   {
     auto &parameter_decl = to_verilog_parameter_decl(module_item);
     collect_symbols(parameter_decl.type());
-    for(auto &decl : parameter_decl.declarations())
-      collect_symbols(parameter_decl.type(), decl);
+    for(auto &declarator : parameter_decl.declarators())
+      collect_symbols(parameter_decl.type(), declarator);
   }
   else if(module_item.id() == ID_local_parameter_decl)
   {
     auto &localparam_decl = to_verilog_local_parameter_decl(module_item);
     collect_symbols(localparam_decl.type());
-    for(auto &decl : localparam_decl.declarations())
-      collect_symbols(localparam_decl.type(), decl);
+    for(auto &declarator : localparam_decl.declarators())
+      collect_symbols(localparam_decl.type(), declarator);
   }
   else if(module_item.id() == ID_decl)
   {
@@ -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';
@@ -146,19 +146,19 @@ static void dependencies_rec(
   else if(module_item.id() == ID_parameter_decl)
   {
     auto &parameter_decl = to_verilog_parameter_decl(module_item);
-    for(auto &decl : parameter_decl.declarations())
+    for(auto &declarator : parameter_decl.declarators())
     {
-      dependencies_rec(decl.type(), dest);
-      dependencies_rec(decl.value(), dest);
+      dependencies_rec(declarator.type(), dest);
+      dependencies_rec(declarator.value(), dest);
     }
   }
   else if(module_item.id() == ID_local_parameter_decl)
   {
     auto &localparam_decl = to_verilog_local_parameter_decl(module_item);
-    for(auto &decl : localparam_decl.declarations())
+    for(auto &declarator : localparam_decl.declarators())
     {
-      dependencies_rec(decl.type(), dest);
-      dependencies_rec(decl.value(), dest);
+      dependencies_rec(declarator.type(), dest);
+      dependencies_rec(declarator.value(), dest);
     }
   }
   else if(module_item.id() == ID_decl)

src/verilog/verilog_expr.h

@@ -680,6 +680,7 @@ class verilog_declaratort : public exprt
 
 using verilog_declaratorst = std::vector<verilog_declaratort>;
 
+/// a SystemVerilog parameter declaration
 class verilog_parameter_declt : public verilog_module_itemt
 {
 public:
@@ -690,12 +691,12 @@ class verilog_parameter_declt : public verilog_module_itemt
   using declaratort = verilog_declaratort;
   using declaratorst = verilog_declaratorst;
 
-  const declaratorst &declarations() const
+  const declaratorst &declarators() const
   {
     return (const declaratorst &)operands();
   }
 
-  declaratorst &declarations()
+  declaratorst &declarators()
   {
     return (declaratorst &)operands();
   }
@@ -725,12 +726,12 @@ class verilog_local_parameter_declt : public verilog_module_itemt
   using declaratort = verilog_declaratort;
   using declaratorst = verilog_declaratorst;
 
-  const declaratorst &declarations() const
+  const declaratorst &declarators() const
   {
     return (const declaratorst &)operands();
   }
 
-  declaratorst &declarations()
+  declaratorst &declarators()
   {
     return (declaratorst &)operands();
   }
@@ -2354,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,18 +33,19 @@ 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();
 
   for(auto &item : module_items)
     if(item.id() == ID_parameter_decl)
-      for(auto &decl : to_verilog_parameter_decl(item).declarations())
-        declarators.push_back(decl);
+      for(auto &declarator : to_verilog_parameter_decl(item).declarators())
+        declarators.push_back(declarator);
 
   return declarators;
 }
@@ -155,33 +156,36 @@ 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();
 
   for(auto &module_item : module_items)
     if(module_item.id() == ID_parameter_decl)
     {
-      for(auto &decl : to_verilog_parameter_decl(module_item).declarations())
+      for(auto &declarator :
+          to_verilog_parameter_decl(module_item).declarators())
       {
         if(p_it!=parameter_values.end())
         {
           DATA_INVARIANT(p_it != parameter_values.end(), "have enough parameter values");
 
           // only overwrite when actually assigned
           if(p_it->is_not_nil())
-            decl.value() = *p_it;
+            declarator.value() = *p_it;
 
           p_it++;
         }

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();