Merge pull request #359 from diffblue/elaborate-wire

Verilog: elaborate wire symbols
This commit is contained in:
Daniel Kroening 2024-02-01 11:05:47 -08:00 committed by GitHub
commit 8e5fe441f3
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
5 changed files with 66 additions and 230 deletions

View File

@ -1,4 +1,4 @@
KNOWNBUG
CORE
wire_bits.v
--bound 0
^EXIT=0$

View File

@ -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)
{

View File

@ -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<const verilog_module_itemt &>(
static_cast<const exprt &>(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:

View File

@ -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)
{

View File

@ -115,7 +115,6 @@ protected:
// 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 @@ protected:
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);