Skip to content

Commit

Permalink
Verilog: constant folding for indexed part select expressions
Browse files Browse the repository at this point in the history
This implements constant folding for indexed part select expressions,
following the pattern in #766.

Fixes #784.
  • Loading branch information
kroening committed Oct 23, 2024
1 parent 37b32b8 commit 460bae6
Show file tree
Hide file tree
Showing 5 changed files with 93 additions and 48 deletions.
2 changes: 2 additions & 0 deletions regression/verilog/expressions/part-select-constant1.sv
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@ module main;
// part-select expressions yield constants
parameter p = 'b1010;
parameter q = p[3:1];
parameter r = p[1 +: 3];

assert final (q == 'b101);
assert final (r == 'b101);

endmodule
79 changes: 79 additions & 0 deletions src/verilog/verilog_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -168,3 +168,82 @@ exprt verilog_non_indexed_part_select_exprt::lower() const
{
return ::lower(*this);
}

static exprt
lower(const verilog_indexed_part_select_plus_or_minus_exprt &part_select)
{
auto get_width = [](const typet &t) -> mp_integer
{
if(t.id() == ID_bool)
return 1;

if(
t.id() == ID_unsignedbv || t.id() == ID_signedbv ||
t.id() == ID_verilog_signedbv || t.id() == ID_verilog_unsignedbv)
{
return to_bitvector_type(t).get_width();
}

PRECONDITION(false);
};

PRECONDITION(
part_select.id() == ID_verilog_indexed_part_select_plus ||
part_select.id() == ID_verilog_indexed_part_select_minus);

const exprt &src = part_select.src();

mp_integer src_width = get_width(src.type());
mp_integer src_offset = string2integer(src.type().get_string(ID_C_offset));

// The width of the indexed part select must be an
// elaboration-time constant.
auto width =
numeric_cast_v<mp_integer>(to_constant_expr(part_select.width()));

// The index need not be a constant.
const exprt &index = part_select.index();

if(index.is_constant())
{
auto index_int = numeric_cast_v<mp_integer>(to_constant_expr(index));

// Construct the extractbits expression
mp_integer bottom, top;

if(part_select.id() == ID_verilog_indexed_part_select_plus)
{
bottom = index_int - src_offset;
top = bottom + width - 1;
}
else // ID_verilog_indexed_part_select_minus
{
top = index_int - src_offset;
bottom = bottom - width + 1;
}

return extractbits_exprt{
std::move(src), from_integer(bottom, integer_typet{}), part_select.type()}
.with_source_location(part_select);
}
else
{
// Index not constant.
// Use logical right-shift followed by (constant) extractbits.
auto index_adjusted =
minus_exprt{index, from_integer(src_offset, index.type())};

auto src_shifted = lshr_exprt(src, index_adjusted);

return extractbits_exprt{
std::move(src_shifted),
from_integer(0, integer_typet{}),
part_select.type()}
.with_source_location(part_select);
}
}

exprt verilog_indexed_part_select_plus_or_minus_exprt::lower() const
{
return ::lower(*this);
}
2 changes: 2 additions & 0 deletions src/verilog/verilog_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -2280,6 +2280,8 @@ class verilog_indexed_part_select_plus_or_minus_exprt : public ternary_exprt
{
return op2();
}

exprt lower() const;
};

inline const verilog_indexed_part_select_plus_or_minus_exprt &
Expand Down
49 changes: 1 addition & 48 deletions src/verilog/verilog_synthesis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -358,54 +358,7 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
expr.id() == ID_verilog_indexed_part_select_minus)
{
auto &part_select = to_verilog_indexed_part_select_plus_or_minus_expr(expr);
exprt &src = part_select.src();

mp_integer src_width = get_width(src.type());
mp_integer src_offset = string2integer(src.type().get_string(ID_C_offset));

// The width of the indexed part select must be an
// elaboration-time constant.
auto width =
numeric_cast_v<mp_integer>(to_constant_expr(part_select.width()));

// The index need not be a constant.
exprt &index = part_select.index();

if(index.is_constant())
{
auto index_int = numeric_cast_v<mp_integer>(to_constant_expr(index));

// Construct the extractbits expression
mp_integer bottom, top;

if(part_select.id() == ID_verilog_indexed_part_select_plus)
{
bottom = index_int - src_offset;
top = bottom + width - 1;
}
else // ID_verilog_indexed_part_select_minus
{
top = index_int - src_offset;
bottom = bottom - width + 1;
}

return extractbits_exprt{
std::move(src), from_integer(bottom, integer_typet{}), expr.type()}
.with_source_location(expr);
}
else
{
// Index not constant.
// Use logical right-shift followed by (constant) extractbits.
auto index_adjusted =
minus_exprt{index, from_integer(src_offset, index.type())};

auto src_shifted = lshr_exprt(src, index_adjusted);

return extractbits_exprt{
std::move(src_shifted), from_integer(0, integer_typet{}), expr.type()}
.with_source_location(expr);
}
return part_select.lower();
}
else if(expr.id() == ID_verilog_logical_equality)
{
Expand Down
9 changes: 9 additions & 0 deletions src/verilog/verilog_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1660,6 +1660,15 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)
auto &part_select = to_verilog_non_indexed_part_select_expr(expr);
expr = part_select.lower();
}
else if(
expr.id() == ID_verilog_indexed_part_select_plus ||
expr.id() == ID_verilog_indexed_part_select_minus)
{
// Our simplifier does not know these, do lowering.
auto &part_select =
to_verilog_indexed_part_select_plus_or_minus_expr(expr);
expr = part_select.lower();
}
else if(expr.id() == ID_reduction_or)
{
// The simplifier doesn't know how to simplify reduction_or
Expand Down

0 comments on commit 460bae6

Please sign in to comment.