Skip to content

Commit

Permalink
Merge pull request #466 from diffblue/use-verilog_inst_baset-instancet
Browse files Browse the repository at this point in the history
Introduce `verilog_inst_baset::named_port_connectiont`
  • Loading branch information
tautschnig authored Apr 30, 2024
2 parents 88381b0 + 086256a commit 4008a86
Show file tree
Hide file tree
Showing 5 changed files with 108 additions and 28 deletions.
9 changes: 9 additions & 0 deletions regression/verilog/modules/inout_and_variable.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
KNOWNBUG
inout_and_variable.v

^file .* line 4: symbol `some_var' is declared both as input and as register$
^EXIT=2$
^SIGNAL=0$
--
--
The use of a variable with an inout port should be rejected.
12 changes: 12 additions & 0 deletions regression/verilog/modules/inout_and_variable.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
module sub(inout some_port);

endmodule

module main;
// 1800-2017 6.5
// "Variables cannot be connected to either side of an inout port"
reg my_var;

sub sub(my_var);

endmodule
54 changes: 54 additions & 0 deletions src/verilog/verilog_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -573,6 +573,39 @@ class verilog_inst_baset : public verilog_module_itemt
return set(ID_module, module);
}

class named_port_connectiont : public binary_exprt
{
public:
named_port_connectiont(exprt _port, exprt _value)
: binary_exprt(
std::move(_port),
ID_named_port_connection,
std::move(_value),
typet{})
{
}

const exprt &port() const
{
return op0();
}

exprt &port()
{
return op0();
}

const exprt &value() const
{
return op1();
}

exprt &value()
{
return op1();
}
};

class instancet : public exprt
{
public:
Expand All @@ -596,6 +629,11 @@ class verilog_inst_baset : public verilog_module_itemt
return operands();
}

exprt::operandst &connections()
{
return operands();
}

protected:
using exprt::operands;
};
Expand All @@ -616,6 +654,22 @@ class verilog_inst_baset : public verilog_module_itemt
using exprt::operands;
};

inline const verilog_inst_baset::named_port_connectiont &
to_verilog_named_port_connection(const exprt &expr)
{
PRECONDITION(expr.id() == ID_named_port_connection);
verilog_inst_baset::named_port_connectiont::check(expr);
return static_cast<const verilog_inst_baset::named_port_connectiont &>(expr);
}

inline verilog_inst_baset::named_port_connectiont &
to_verilog_named_port_connection(exprt &expr)
{
PRECONDITION(expr.id() == ID_named_port_connection);
verilog_inst_baset::named_port_connectiont::check(expr);
return static_cast<verilog_inst_baset::named_port_connectiont &>(expr);
}

class verilog_instt : public verilog_inst_baset
{
public:
Expand Down
55 changes: 30 additions & 25 deletions src/verilog/verilog_typecheck.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ Function: verilog_typecheckt::typecheck_port_connections
\*******************************************************************/

void verilog_typecheckt::typecheck_port_connections(
exprt &inst,
verilog_inst_baset::instancet &inst,
const symbolt &symbol)
{
const exprt &range=static_cast<const exprt &>(inst.find(ID_range));
Expand All @@ -92,12 +92,15 @@ void verilog_typecheckt::typecheck_port_connections(

const irept::subt &ports=symbol.type.find(ID_ports).get_sub();

// no arguments is one argument that is nil
if(ports.size()==0 && inst.operands().size()==1 &&
inst.operands().front().is_nil())
inst.operands().clear();
// no arguments is one argument that is nil
if(
ports.size() == 0 && inst.connections().size() == 1 &&
inst.connections().front().is_nil())
{
inst.connections().clear();
}

if(inst.operands().empty())
if(inst.connections().empty())
{
if(!ports.empty())
{
Expand All @@ -110,35 +113,37 @@ void verilog_typecheckt::typecheck_port_connections(

// named port connection?

if(to_multi_ary_expr(inst).op0().id() == ID_named_port_connection)
if(inst.connections().front().id() == ID_named_port_connection)
{
// We don't require that all ports are connected.

std::set<irep_idt> assigned_ports;

Forall_operands(o_it, inst)
for(auto &connection : inst.connections())
{
if(o_it->id()!=ID_named_port_connection ||
o_it->operands().size()!=2)
if(connection.id() != ID_named_port_connection)
{
throw errort().with_location(inst.source_location())
<< "expected a named port connection";
}

exprt &op = to_binary_expr(*o_it).op1();
const irep_idt &name = to_binary_expr(*o_it).op0().get(ID_identifier);
auto &named_port_connection =
to_verilog_named_port_connection(connection);

exprt &value = named_port_connection.value();
const irep_idt &name = named_port_connection.port().get(ID_identifier);

bool found=false;

std::string identifier=
id2string(symbol.module)+"."+id2string(name);

to_binary_expr(*o_it).op0().set(ID_identifier, identifier);
named_port_connection.port().set(ID_identifier, identifier);

if(assigned_ports.find(name)!=
assigned_ports.end())
{
throw errort().with_location(o_it->source_location())
throw errort().with_location(connection.source_location())
<< "port name " << name << " assigned twice";
}

Expand All @@ -148,15 +153,15 @@ void verilog_typecheckt::typecheck_port_connections(
{
auto &p_expr = static_cast<const exprt &>(port);
found=true;
typecheck_port_connection(op, p_expr);
to_binary_expr(*o_it).op0().type() = p_expr.type();
typecheck_port_connection(value, p_expr);
named_port_connection.port().type() = p_expr.type();
break;
}
}

if(!found)
{
throw errort().with_location(o_it->source_location())
throw errort().with_location(connection.source_location())
<< "port name " << identifier << " not found";
}

Expand All @@ -165,19 +170,19 @@ void verilog_typecheckt::typecheck_port_connections(
}
else // just a list without names
{
if(inst.operands().size()!=ports.size())
if(inst.connections().size() != ports.size())
{
throw errort().with_location(inst.source_location())
<< "wrong number of arguments: expected " << ports.size() << " but got "
<< inst.operands().size();
<< inst.connections().size();
}

irept::subt::const_iterator p_it=
ports.begin();

Forall_operands(o_it, inst)
for(auto &connection : inst.connections())
{
typecheck_port_connection(*o_it, (exprt &)*p_it);
typecheck_port_connection(connection, (exprt &)*p_it);
p_it++;
}
}
Expand All @@ -196,7 +201,7 @@ Function: verilog_typecheckt::typecheck_builtin_port_connections
\*******************************************************************/

void verilog_typecheckt::typecheck_builtin_port_connections(
exprt &inst)
verilog_inst_baset::instancet &inst)
{
exprt &range=static_cast<exprt &>(inst.add(ID_range));

Expand All @@ -221,10 +226,10 @@ void verilog_typecheckt::typecheck_builtin_port_connections(
type.set(ID_width, integer2string(width));
}

Forall_operands(o_it, inst)
for(auto &connection : inst.connections())
{
convert_expr(*o_it);
propagate_type(*o_it, type);
convert_expr(connection);
propagate_type(connection, type);
}
}

Expand Down
6 changes: 3 additions & 3 deletions src/verilog/verilog_typecheck.h
Original file line number Diff line number Diff line change
Expand Up @@ -177,15 +177,15 @@ class verilog_typecheckt:

void instantiate_port_connections(
const std::string &instance,
const exprt &inst,
const verilog_inst_baset::instancet &,
const symbolt &symbol,
exprt &trans);

void typecheck_port_connections(
exprt &inst,
verilog_inst_baset::instancet &,
const symbolt &symbol);

void typecheck_builtin_port_connections(exprt &inst);
void typecheck_builtin_port_connections(verilog_inst_baset::instancet &);

void typecheck_port_connection(
exprt &op,
Expand Down

0 comments on commit 4008a86

Please sign in to comment.