From 720b41d06d1e2439cc486c3e1bfa30d45eea26c9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 30 Jan 2024 07:17:51 -0800 Subject: [PATCH] Verilog: elaborate wire symbols This moves the creation of wire symbols from verilog_interfaces to the elaboration phase. --- regression/verilog/elaboration/wire_bits.desc | 2 +- src/verilog/verilog_elaborate.cpp | 65 ++++++++ src/verilog/verilog_generate.cpp | 78 --------- src/verilog/verilog_interfaces.cpp | 148 ------------------ src/verilog/verilog_typecheck.h | 3 - 5 files changed, 66 insertions(+), 230 deletions(-) diff --git a/regression/verilog/elaboration/wire_bits.desc b/regression/verilog/elaboration/wire_bits.desc index c97fee0f5..03dc2da1c 100644 --- a/regression/verilog/elaboration/wire_bits.desc +++ b/regression/verilog/elaboration/wire_bits.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE wire_bits.v --bound 0 ^EXIT=0$ diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 74dd5adba..ab0a9decb 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -368,6 +368,71 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) decl_class == ID_tri0 || decl_class == ID_tri1 || decl_class == ID_uwire || decl_class == ID_wire || decl_class == ID_wand || decl_class == ID_wor) { + symbolt symbol; + + symbol.mode = mode; + symbol.module = module_identifier; + symbol.value = nil_exprt(); + + auto type = convert_type(decl.type()); + + for(auto &declarator : decl.declarators()) + { + DATA_INVARIANT(declarator.id() == ID_declarator, "must have declarator"); + + symbol.base_name = declarator.base_name(); + symbol.location = declarator.source_location(); + + if(declarator.type().is_nil()) + symbol.type = type; + else if(declarator.type().id() == ID_array) + symbol.type = array_type(declarator.type(), type); + else + { + throw errort().with_location(symbol.location) + << "unexpected type on declarator"; + } + + if(symbol.base_name.empty()) + { + throw errort().with_location(decl.source_location()); + error() << "empty symbol name" << eom; + } + + symbol.name = hierarchical_identifier(symbol.base_name); + symbol.pretty_name = strip_verilog_prefix(symbol.name); + + auto result = symbol_table.get_writeable(symbol.name); + + if(result == nullptr) + { + // new identifier + symbol_table.add(symbol); + } + else + { + // We have an existing symbol with that name. + // This is ok for certain symbols, e.g., input/wire, output/reg. + symbolt &osymbol = *result; + + if(osymbol.type.id() == ID_code) + { + error().source_location = decl.source_location(); + error() << "symbol `" << symbol.base_name << "' is already declared" + << eom; + throw 0; + } + + // change of type? + if(symbol.type != osymbol.type) + { + if(get_width(symbol.type) > get_width(osymbol.type)) + osymbol.type = symbol.type; + } + } + + symbols_added.push_back(symbol.name); + } } else if(decl_class == ID_reg || decl_class == ID_var) { diff --git a/src/verilog/verilog_generate.cpp b/src/verilog/verilog_generate.cpp index a7724ed63..202eae43e 100644 --- a/src/verilog/verilog_generate.cpp +++ b/src/verilog/verilog_generate.cpp @@ -51,84 +51,6 @@ void verilog_typecheckt::elaborate_generate_block( /*******************************************************************\ -Function: verilog_typecheckt::elaborate_generate_decl - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void verilog_typecheckt::elaborate_generate_decl( - const verilog_declt &decl, - module_itemst &dest) -{ - auto decl_class = decl.get_class(); - - if(decl_class == ID_verilog_genvar) - { - // Assign to "-1", which signals "the variable is unset" - for(auto &declarator : decl.declarators()) - genvars[declarator.identifier()] = -1; - } - else - { - if(decl_class == ID_reg || decl_class == ID_wire) - { - // verilog_typecheckt::module_interfaces does not add - // symbols in generate blocks, since the generate blocks - // have not yet been elaborated. Do so now. - interface_module_decl(decl); - } - - // Preserve the declaration for any initializers. - verilog_set_genvarst tmp(static_cast( - static_cast(decl))); - auto &variables = tmp.variables(); - - for(const auto &it : genvars) - variables[it.first] = irept(integer2string(it.second)); - - dest.push_back(std::move(tmp)); - } -} - -/*******************************************************************\ - -Function: verilog_typecheckt::elaborate_generate_inst - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void verilog_typecheckt::elaborate_generate_inst( - const verilog_instt &inst, - module_itemst &dest) -{ - // verilog_typecheckt::module_interfaces does not add - // symbols for module instances in generate blocks, - // since the generate blocks have not yet been elaborated. - // Do so now. - interface_inst(inst); - - // Preserve the instantiation - verilog_set_genvarst tmp(inst); - auto &variables = tmp.variables(); - - for(const auto &it : genvars) - variables[it.first] = irept(integer2string(it.second)); - - dest.push_back(std::move(tmp)); -} - -/*******************************************************************\ - Function: verilog_typecheckt::elaborate_generate_item Inputs: diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index 58b858d13..db5d41d93 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -136,150 +136,6 @@ void verilog_typecheckt::check_module_ports( /*******************************************************************\ -Function: verilog_typecheckt::interface_module_decl - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void verilog_typecheckt::interface_module_decl( - const verilog_declt &decl) -{ - assert(function_or_task_name==""); - - symbolt symbol; - typet type; - - symbol.mode=mode; - symbol.module=module_identifier; - symbol.value.make_nil(); - const irep_idt &port_class=decl.get_class(); - - if(port_class==ID_function || - port_class==ID_task) - { - // symbols already created during elaboration - return; - } - else if( - port_class == ID_input || port_class == ID_output || - port_class == ID_output_register || port_class == ID_inout || - port_class == ID_verilog_genvar || port_class == ID_reg || - port_class == ID_var) - { - // symbol already created during elaboration - return; - } - else - { - type=convert_type(decl.type()); - - if(port_class == ID_reg || port_class == ID_var) - symbol.is_state_var=true; - else if(port_class==ID_wire) - { - } - else if(port_class == ID_supply0) - { - } - else if(port_class == ID_supply1) - { - } - else if(port_class == ID_typedef) - { - symbol.is_type = true; - } - else - { - if( - type.id() == ID_integer || type.id() == ID_verilog_realtime || - type.id() == ID_verilog_shortreal || type.id() == ID_verilog_real) - { - symbol.is_lvalue = true; - } - else - { - error().source_location = decl.source_location(); - error() << "unexpected port class: `" << port_class << '\'' << eom; - throw 0; - } - } - } - - for(auto &declarator : decl.declarators()) - { - DATA_INVARIANT(declarator.id() == ID_declarator, "must have declarator"); - - symbol.base_name = declarator.base_name(); - symbol.location = declarator.source_location(); - - if(declarator.type().is_nil()) - symbol.type=type; - else if(declarator.type().id() == ID_array) - symbol.type = array_type(declarator.type(), type); - else - { - error().source_location = symbol.location; - error() << "unexpected type on declarator" << eom; - throw 0; - } - - if(symbol.base_name.empty()) - { - error().source_location = decl.source_location(); - error() << "empty symbol name" << eom; - throw 0; - } - - symbol.name = hierarchical_identifier(symbol.base_name); - symbol.pretty_name = strip_verilog_prefix(symbol.name); - - auto result=symbol_table.get_writeable(symbol.name); - - if(result==nullptr) - { - symbol_table.add(symbol); - } - else - { - symbolt &osymbol=*result; - - if(osymbol.type.id()==ID_code) - { - error().source_location = decl.source_location(); - error() << "symbol `" << symbol.base_name - << "' is already declared" << eom; - throw 0; - } - - if(symbol.type!=osymbol.type) - { - if(get_width(symbol.type)>get_width(osymbol.type)) - osymbol.type=symbol.type; - } - - osymbol.is_input =symbol.is_input || osymbol.is_input; - osymbol.is_output =symbol.is_output || osymbol.is_output; - osymbol.is_state_var=symbol.is_state_var || osymbol.is_state_var; - - // a register can't be an input as well - if(osymbol.is_input && osymbol.is_state_var) - { - error().source_location = decl.source_location(); - error() << "symbol `" << symbol.base_name - << "' is declared both as input and as register" << eom; - throw 0; - } - } - } -} - -/*******************************************************************\ - Function: verilog_typecheckt::convert_inst Inputs: @@ -395,8 +251,6 @@ void verilog_typecheckt::interface_module_item( { if(module_item.id()==ID_decl) { - if(function_or_task_name.empty()) - interface_module_decl(to_verilog_decl(module_item)); } else if(module_item.id()==ID_parameter_decl || module_item.id()==ID_local_parameter_decl) @@ -458,8 +312,6 @@ void verilog_typecheckt::interface_statement( } else if(statement.id()==ID_decl) { - if(function_or_task_name.empty()) - interface_module_decl(to_verilog_decl(statement)); } else if(statement.id()==ID_event_guard) { diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index d8c115539..7f99e7b4a 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -115,7 +115,6 @@ class verilog_typecheckt: // interfaces void module_interface(const verilog_module_sourcet &); void check_module_ports(const verilog_module_sourcet::port_listt &); - void interface_module_decl(const class verilog_declt &); void interface_inst(const verilog_inst_baset &); void interface_inst( const verilog_inst_baset &, @@ -205,8 +204,6 @@ class verilog_typecheckt: void elaborate_generate_block( const verilog_generate_blockt &, module_itemst &dest); - void elaborate_generate_decl(const verilog_declt &, module_itemst &dest); - void elaborate_generate_inst(const verilog_instt &, module_itemst &dest); module_itemst elaborate_generate_item(const verilog_module_itemt &); void elaborate_generate_item(const verilog_module_itemt &src, module_itemst &dest);