diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index bf8fdad18..15011d03d 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/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) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 94c8d7da5..af3964c6b 100644 --- a/src/verilog/parser.y +++ b/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: diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 69ccd8b6a..bf3b9bf37 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -804,15 +804,15 @@ void verilog_typecheckt::collect_symbols( { auto ¶meter_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 ¶meter_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. diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index f1ca0e9d3..3727917a9 100644 --- a/src/verilog/verilog_expr.cpp +++ b/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 ¶meter : parameter_port_list()) + for(auto ¶meter : 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 ¶meter_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) diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index e87912694..3859ae2d8 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -680,6 +680,7 @@ class verilog_declaratort : public exprt using verilog_declaratorst = std::vector; +/// 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; - const parameter_port_listt ¶meter_port_list() const + const parameter_port_declst ¶meter_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 ¶meter_port_list() + parameter_port_declst ¶meter_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; diff --git a/src/verilog/verilog_parameterize_module.cpp b/src/verilog/verilog_parameterize_module.cpp index 21d101db1..e390bbea2 100644 --- a/src/verilog/verilog_parameterize_module.cpp +++ b/src/verilog/verilog_parameterize_module.cpp @@ -33,18 +33,19 @@ verilog_typecheckt::get_parameter_declarators( std::vector declarators; // We do the parameter ports first. - const auto ¶meter_port_list = module_source.parameter_port_list(); + const auto ¶meter_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,25 +156,28 @@ void verilog_typecheckt::set_parameter_values( { auto p_it=parameter_values.begin(); - auto ¶meter_port_list = module_source.parameter_port_list(); + auto ¶meter_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()) { @@ -181,7 +185,7 @@ void verilog_typecheckt::set_parameter_values( // only overwrite when actually assigned if(p_it->is_not_nil()) - decl.value() = *p_it; + declarator.value() = *p_it; p_it++; } diff --git a/src/verilog/verilog_parse_tree.cpp b/src/verilog/verilog_parse_tree.cpp index f796bd512..61655f0c1 100644 --- a/src/verilog/verilog_parse_tree.cpp +++ b/src/verilog/verilog_parse_tree.cpp @@ -25,7 +25,7 @@ exprt verilog_parse_treet::create_module( irept &attributes, irept &module_keyword, exprt &name, - exprt ¶meter_port_list, + exprt ¶meter_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();