Skip to content

Verilog: get_width now returns mp_integer #417

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Mar 18, 2024
Merged

Verilog: get_width now returns mp_integer #417

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
29 changes: 15 additions & 14 deletions src/verilog/verilog_synthesis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -299,33 +299,33 @@ void verilog_synthesist::assignment_rec(
{
// TODO: split it up more intelligently;
// bit-wise is wasteful.
unsigned offset=0;
mp_integer offset = 0;

// do it from right to left

for(exprt::operandst::const_reverse_iterator
it=lhs.operands().rbegin();
it!=lhs.operands().rend();
it++)
{
constant_exprt offset_constant{std::to_string(offset), natural_typet{}};
auto offset_constant = from_integer(offset, natural_typet{});

if(it->type().id()==ID_bool)
{
exprt bit_extract(ID_extractbit, it->type());
bit_extract.add_to_operands(rhs);
bit_extract.add_to_operands(offset_constant);
offset++;
++offset;

assignment_rec(*it, bit_extract, blocking);
}
else if(it->type().id()==ID_signedbv ||
it->type().id()==ID_unsignedbv)
{
unsigned width=get_width(it->type());
auto width = get_width(it->type());

constant_exprt offset_constant2{std::to_string(offset + width - 1),
natural_typet{}};
auto offset_constant2 =
from_integer(offset + width - 1, natural_typet{});

// extractbits requires that upper >= lower, i.e. op1 >= op2
extractbits_exprt bit_extract(rhs, offset_constant2, offset_constant,
Expand Down Expand Up @@ -1682,29 +1682,30 @@ void verilog_synthesist::synth_force_rec(
if(lhs.id()==ID_concatenation)
{
// split it up
unsigned offset=0;
mp_integer offset = 0;

// do it from right to left

for(exprt::operandst::const_reverse_iterator
it=lhs.operands().rbegin();
it!=lhs.operands().rend();
it++)
{
constant_exprt offset_constant{std::to_string(offset), natural_typet{}};
auto offset_constant = from_integer(offset, natural_typet{});

if(it->type().id()==ID_bool)
{
extractbit_exprt bit_extract(rhs, offset);
offset++;
extractbit_exprt bit_extract(rhs, offset_constant);
++offset;
synth_force_rec(*it, bit_extract);
}
else if(it->type().id()==ID_signedbv ||
it->type().id()==ID_unsignedbv)
{
unsigned width=get_width(it->type());
auto width = get_width(it->type());
auto sum_constant = from_integer(offset + width - 1, natural_typet{});
extractbits_exprt bit_extract(
rhs, offset, offset + width - 1, it->type());
rhs, offset_constant, sum_constant, it->type());
synth_force_rec(*it, bit_extract);
offset+=width;
}
Expand Down
4 changes: 2 additions & 2 deletions src/verilog/verilog_typecheck_base.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,7 @@ Function: verilog_typecheck_baset::get_width

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

std::size_t verilog_typecheck_baset::get_width(const typet &type)
mp_integer verilog_typecheck_baset::get_width(const typet &type)
{
if(type.id()==ID_bool)
return 1;
Expand All @@ -188,7 +188,7 @@ std::size_t verilog_typecheck_baset::get_width(const typet &type)
mp_integer sum = 0;
for(auto &component : to_struct_type(type).components())
sum += get_width(component.type());
return sum.to_ulong();
return sum;
}

if(type.id() == ID_verilog_shortint)
Expand Down
9 changes: 6 additions & 3 deletions src/verilog/verilog_typecheck_base.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,9 +38,12 @@ class verilog_typecheck_baset:public typecheckt
protected:
const namespacet &ns;
const irep_idt mode;

std::size_t get_width(const exprt &expr) { return get_width(expr.type()); }
std::size_t get_width(const typet &type);

mp_integer get_width(const exprt &expr)
{
return get_width(expr.type());
}
mp_integer get_width(const typet &type);
mp_integer array_size(const array_typet &);
mp_integer array_offset(const array_typet &);
typet index_type(const array_typet &);
Expand Down
43 changes: 23 additions & 20 deletions src/verilog/verilog_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -266,8 +266,8 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
throw errort().with_location(expr.source_location())
<< "concatenation expected to have at least one operand";
}
unsigned width=0;

mp_integer width = 0;
bool has_verilogbv=false;

Forall_operands(it, expr)
Expand Down Expand Up @@ -300,23 +300,24 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
if(op.type().id() == ID_signedbv || op.type().id() == ID_verilog_signedbv)
{
auto width = get_width(op);
auto width_int = numeric_cast_v<std::size_t>(width);
if(op.type().id() == ID_verilog_signedbv)
op = typecast_exprt(op, verilog_unsignedbv_typet(width));
op = typecast_exprt{op, verilog_unsignedbv_typet{width_int}};
else
op = typecast_exprt(op, unsignedbv_typet(width));
op = typecast_exprt{op, unsignedbv_typet{width_int}};
}
}

expr.type()=typet(has_verilogbv?ID_verilog_unsignedbv:ID_unsignedbv);
expr.type().set(ID_width, width);
expr.type().set(ID_width, integer2string(width));

if(has_verilogbv)
{
Forall_operands(it, expr)
if(it->type().id()!=ID_verilog_unsignedbv)
{
unsigned width=get_width(*it);
*it = typecast_exprt{*it, verilog_unsignedbv_typet{width}};
auto width_int = numeric_cast_v<std::size_t>(get_width(*it));
*it = typecast_exprt{*it, verilog_unsignedbv_typet{width_int}};
}
}

Expand Down Expand Up @@ -2045,13 +2046,14 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr)
{
expr.op0()=from_integer(op0, natural_typet());

std::size_t new_width = op0.to_ulong() * width;
auto new_width = op0 * width;
auto new_width_int = numeric_cast_v<std::size_t>(new_width);

if(op1.type().id()==ID_verilog_unsignedbv ||
op1.type().id()==ID_verilog_signedbv)
expr.type()=verilog_unsignedbv_typet(new_width);
expr.type() = verilog_unsignedbv_typet{new_width_int};
else
expr.type()=unsignedbv_typet(new_width);
expr.type() = unsignedbv_typet{new_width_int};
}

return std::move(expr);
Expand Down Expand Up @@ -2327,10 +2329,10 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
if(op2 < offset)
{
auto padding_width = offset - op2;
auto padding =
from_integer(0, unsignedbv_typet{(padding_width).to_ulong()});
auto new_type =
unsignedbv_typet{(get_width(op0.type()) + padding_width).to_ulong()};
auto padding = from_integer(
0, unsignedbv_typet{numeric_cast_v<std::size_t>(padding_width)});
auto new_type = unsignedbv_typet{
numeric_cast_v<std::size_t>(get_width(op0.type()) + padding_width)};
expr.op0() = concatenation_exprt(expr.op0(), padding, new_type);
op2 += padding_width;
op1 += padding_width;
Expand All @@ -2339,16 +2341,17 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
if(op1 >= width + offset)
{
auto padding_width = op1 - (width + offset) + 1;
auto padding =
from_integer(0, unsignedbv_typet{padding_width.to_ulong()});
auto new_type =
unsignedbv_typet{(get_width(op0.type()) + padding_width).to_ulong()};
auto padding = from_integer(
0, unsignedbv_typet{numeric_cast_v<std::size_t>(padding_width)});
auto new_type = unsignedbv_typet{
numeric_cast_v<std::size_t>(get_width(op0.type()) + padding_width)};
expr.op0() = concatenation_exprt(padding, expr.op0(), new_type);
}

// Part-select expressions are unsigned, even if the
// entire expression is selected!
auto expr_type = unsignedbv_typet((op1 - op2).to_ulong() + 1);
auto expr_type =
unsignedbv_typet{numeric_cast_v<std::size_t>(op1 - op2 + 1)};

op2 -= offset;
op1 -= offset;
Expand Down
6 changes: 4 additions & 2 deletions src/verilog/verilog_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,8 @@ class verilog_signedbv_typet:public bitvector_typet
{
}

explicit inline verilog_signedbv_typet(unsigned width):bitvector_typet(ID_verilog_signedbv, width)
explicit inline verilog_signedbv_typet(std::size_t width)
: bitvector_typet(ID_verilog_signedbv, width)
{
}
};
Expand Down Expand Up @@ -102,7 +103,8 @@ class verilog_unsignedbv_typet:public bitvector_typet
{
}

explicit inline verilog_unsignedbv_typet(unsigned width):bitvector_typet(ID_verilog_unsignedbv, width)
explicit inline verilog_unsignedbv_typet(std::size_t width)
: bitvector_typet(ID_verilog_unsignedbv, width)
{
}
};
Expand Down