Skip to content
Draft
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 37 additions & 11 deletions src/trans-netlist/trans_to_netlist.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -141,9 +141,15 @@ class convert_trans_to_netlistt:public messaget

literalt convert_rhs(const rhst &);

void finalize_lhs(lhs_mapt::iterator);

void convert_lhs_rec(const exprt &expr, std::size_t from, std::size_t to);
// The bv_varidts of the definitions that are yet to be processed.
using lhs_stackt = std::stack<bv_varidt>;
void add_to_stack(
const exprt &expr,
std::size_t from,
std::size_t to,
lhs_stackt &);
void lhs_loop(lhs_stackt &);
void finalize_definition(lhs_mapt::iterator);

void convert_constraints();

Expand Down Expand Up @@ -547,7 +553,7 @@ void convert_trans_to_netlistt::finalize_lhs(lhs_mapt::iterator lhs_it)

/*******************************************************************\

Function: convert_trans_to_netlistt::convert_lhs_rec
Function: convert_trans_to_netlistt::lhs_loop

Inputs:

Expand All @@ -557,10 +563,27 @@ Function: convert_trans_to_netlistt::convert_lhs_rec

\*******************************************************************/

void convert_trans_to_netlistt::convert_lhs_rec(
void convert_trans_to_netlistt::lhs_loop(lhs_stackt &lhs_stack)
{
}

/*******************************************************************\

Function: convert_trans_to_netlistt::add_to_stack

Inputs:

Outputs:

Purpose:

\*******************************************************************/

void convert_trans_to_netlistt::add_to_stack(
const exprt &expr,
std::size_t from,
std::size_t to)
std::size_t to,
lhs_stackt &lhs_stack)
{
PRECONDITION(from <= to);

Expand All @@ -574,6 +597,8 @@ void convert_trans_to_netlistt::convert_lhs_rec(
bv_varid.bit_nr<=to;
bv_varid.bit_nr++)
{
lhs_stack.push(bv_varid);
#if 0
lhs_mapt::iterator it=lhs_map.find(bv_varid);

if(it==lhs_map.end())
Expand All @@ -582,8 +607,9 @@ void convert_trans_to_netlistt::convert_lhs_rec(

// we only need to do wires
if(!it->second.var->is_wire()) return;

finalize_lhs(it);
#endif
}

return;
Expand All @@ -595,7 +621,7 @@ void convert_trans_to_netlistt::convert_lhs_rec(
to_extractbit_expr(expr).index(), i)) // constant?
{
from = i.to_ulong();
convert_lhs_rec(to_extractbit_expr(expr).src(), from, from);
add_to_stack(to_extractbit_expr(expr).src(), from, from, lhs_stack);
return;
}
}
Expand All @@ -614,7 +640,7 @@ void convert_trans_to_netlistt::convert_lhs_rec(
from = new_from.to_ulong();
to = new_to.to_ulong();

convert_lhs_rec(to_extractbits_expr(expr).src(), from, to);
add_to_stack(to_extractbits_expr(expr).src(), from, to, lhs_stack);
return;
}
}
Expand All @@ -634,7 +660,7 @@ void convert_trans_to_netlistt::convert_lhs_rec(
if(width==0)
continue;

convert_lhs_rec(*it, 0, width - 1);
add_to_stack(*it, 0, width - 1, lhs_stack);
}
}

Expand All @@ -658,7 +684,7 @@ literalt convert_trans_to_netlistt::convert_rhs(const rhst &rhs)
if(!rhs_entry.converted)
{
// get all lhs symbols this depends on
convert_lhs_rec(rhs_entry.expr, 0, rhs_entry.width - 1);
add_to_stack(rhs_entry.expr, 0, rhs_entry.width - 1, lhs_stack);

rhs_entry.converted=true;

Expand Down
Loading