Skip to content

Introduce sva_sequence_repetition_exprt #1080

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
Apr 24, 2025
Merged

Introduce sva_sequence_repetition_exprt #1080

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
64 changes: 21 additions & 43 deletions src/verilog/expr2verilog.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -608,31 +608,6 @@ expr2verilogt::resultt expr2verilogt::convert_sva_binary(

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

Function: expr2verilogt::convert_sva_binary_repetition

Inputs:

Outputs:

Purpose:

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

expr2verilogt::resultt expr2verilogt::convert_sva_binary_repetition(
const std::string &name,
const binary_exprt &expr)
{
auto op0 = convert_rec(expr.lhs());
if(op0.p == verilog_precedencet::MIN)
op0.s = "(" + op0.s + ")";

auto op1 = convert_rec(expr.rhs());

return {verilog_precedencet::MIN, op0.s + " " + name + op1.s + "]"};
}

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

Function: expr2verilogt::convert_sva_sequence_consecutive_repetition

Inputs:
Expand All @@ -643,20 +618,27 @@ Function: expr2verilogt::convert_sva_sequence_consecutive_repetition

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

expr2verilogt::resultt
expr2verilogt::convert_sva_sequence_consecutive_repetition(
const sva_sequence_consecutive_repetition_exprt &expr)
expr2verilogt::resultt expr2verilogt::convert_sva_sequence_repetition(
const std::string &name,
const sva_sequence_repetition_exprt &expr)
{
auto op = convert_rec(expr.op());
if(op.p == verilog_precedencet::MIN)
op.s = "(" + op.s + ")";

std::string dest = op.s + " [*" + convert_rec(expr.from()).s;
std::string dest = op.s + " [" + name;

if(expr.is_range())
{
dest += convert_rec(expr.from()).s;

if(expr.is_unbounded())
dest += ":$";
else if(expr.to().is_not_nil())
dest += ":" + convert_rec(expr.to()).s;
if(expr.is_unbounded())
dest += ":$";
else
dest += ":" + convert_rec(expr.to()).s;
}
else
dest += convert_rec(expr.repetitions()).s;

dest += ']';

Expand Down Expand Up @@ -1877,20 +1859,16 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
// not sure about precedence

else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
return precedence = verilog_precedencet::MIN,
convert_sva_binary_repetition(
"[=", to_sva_sequence_non_consecutive_repetition_expr(src));
// not sure about precedence
return convert_sva_sequence_repetition(
"=", to_sva_sequence_non_consecutive_repetition_expr(src));

else if(src.id() == ID_sva_sequence_consecutive_repetition)
return convert_sva_sequence_consecutive_repetition(
to_sva_sequence_consecutive_repetition_expr(src));
return convert_sva_sequence_repetition(
"*", to_sva_sequence_consecutive_repetition_expr(src));

else if(src.id() == ID_sva_sequence_goto_repetition)
return precedence = verilog_precedencet::MIN,
convert_sva_binary_repetition(
"[->", to_sva_sequence_goto_repetition_expr(src));
// not sure about precedence
return convert_sva_sequence_repetition(
"->", to_sva_sequence_goto_repetition_expr(src));

else if(src.id() == ID_sva_ranged_always)
{
Expand Down
10 changes: 4 additions & 6 deletions src/verilog/expr2verilog_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ class sva_abort_exprt;
class sva_case_exprt;
class sva_if_exprt;
class sva_ranged_predicate_exprt;
class sva_sequence_consecutive_repetition_exprt;
class sva_sequence_repetition_exprt;
class sva_sequence_first_match_exprt;

// Precedences (higher means binds more strongly).
Expand Down Expand Up @@ -137,11 +137,9 @@ class expr2verilogt

resultt convert_sva_binary(const std::string &name, const binary_exprt &);

resultt
convert_sva_binary_repetition(const std::string &name, const binary_exprt &);

resultt convert_sva_sequence_consecutive_repetition(
const sva_sequence_consecutive_repetition_exprt &);
resultt convert_sva_sequence_repetition(
const std::string &name,
const sva_sequence_repetition_exprt &);

resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &);

Expand Down
20 changes: 18 additions & 2 deletions src/verilog/parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2707,12 +2707,28 @@ consecutive_repetition:

non_consecutive_repetition:
"[=" const_or_range_expression ']'
{ init($$, ID_sva_sequence_non_consecutive_repetition); mto($$, $2); }
{ init($$, ID_sva_sequence_non_consecutive_repetition);
if(stack_expr($2).id() == ID_sva_cycle_delay)
swapop($$, $2);
else
{
mto($$, $2);
stack_expr($$).add_to_operands(nil_exprt{});
}
}
;

goto_repetition:
"[->" const_or_range_expression ']'
{ init($$, ID_sva_sequence_goto_repetition); mto($$, $2); }
{ init($$, ID_sva_sequence_goto_repetition);
if(stack_expr($2).id() == ID_sva_cycle_delay)
swapop($$, $2);
else
{
mto($$, $2);
stack_expr($$).add_to_operands(nil_exprt{});
}
}
;

cycle_delay_range:
Expand Down
10 changes: 5 additions & 5 deletions src/verilog/sva_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,10 +62,10 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const
PRECONDITION(
op().type().id() == ID_bool || op().type().id() == ID_verilog_sva_sequence);

if(to().is_nil())
if(!is_range())
{
// expand x[*n] into x ##1 x ##1 ...
auto n = numeric_cast_v<mp_integer>(to_constant_expr(from()));
auto n = numeric_cast_v<mp_integer>(repetitions());
DATA_INVARIANT(n >= 1, "number of repetitions must be at least one");

exprt result = op();
Expand All @@ -84,11 +84,11 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const
{
PRECONDITION(false);
}
else
else // bounded range
{
// expand x[*a:b] into x[*a] or x[*a+1] or ... or x[*b]
auto from_int = numeric_cast_v<mp_integer>(to_constant_expr(from()));
auto to_int = numeric_cast_v<mp_integer>(to_constant_expr(to()));
auto from_int = numeric_cast_v<mp_integer>(from());
auto to_int = numeric_cast_v<mp_integer>(to());

DATA_INVARIANT(from_int >= 1, "number of repetitions must be at least one");
DATA_INVARIANT(
Expand Down
Loading
Loading