Skip to content

SVA: use from/to instead of lower/upper #1128

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
Jun 4, 2025
Merged

SVA: use from/to instead of lower/upper #1128

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
18 changes: 8 additions & 10 deletions src/ebmc/completeness_threshold.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,13 +39,12 @@ bool has_low_completeness_threshold(const exprt &expr)
auto &always_expr = to_sva_ranged_always_expr(expr);
if(has_temporal_operator(always_expr.op()))
return false;
else if(always_expr.upper().is_constant())
else if(always_expr.to().is_constant())
{
auto lower_int = numeric_cast_v<mp_integer>(always_expr.lower());
auto upper_int =
numeric_cast_v<mp_integer>(to_constant_expr(always_expr.upper()));
return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
upper_int <= 1;
auto from_int = numeric_cast_v<mp_integer>(always_expr.from());
auto to_int =
numeric_cast_v<mp_integer>(to_constant_expr(always_expr.to()));
return from_int >= 0 && from_int <= 1 && to_int >= 0 && to_int <= 1;
}
else
return false;
Expand All @@ -57,10 +56,9 @@ bool has_low_completeness_threshold(const exprt &expr)
return false;
else
{
auto lower_int = numeric_cast_v<mp_integer>(s_always_expr.lower());
auto upper_int = numeric_cast_v<mp_integer>(s_always_expr.upper());
return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
upper_int <= 1;
auto from_int = numeric_cast_v<mp_integer>(s_always_expr.from());
auto to_int = numeric_cast_v<mp_integer>(s_always_expr.to());
return from_int >= 0 && from_int <= 1 && to_int >= 0 && to_int <= 1;
}
}
else if(
Expand Down
22 changes: 11 additions & 11 deletions src/temporal-logic/ltl_sva_to_string.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,16 +161,16 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
{
auto &always = to_sva_ranged_always_expr(expr);
auto new_expr = unary_exprt{ID_sva_ranged_always, always.op()};
auto lower = numeric_cast_v<mp_integer>(always.lower());
auto from = numeric_cast_v<mp_integer>(always.from());
if(!always.is_range())
return prefix("F[" + integer2string(lower) + "]", new_expr, mode);
return prefix("F[" + integer2string(from) + "]", new_expr, mode);
else if(always.is_unbounded())
return prefix("F[" + integer2string(lower) + ":]", new_expr, mode);
return prefix("F[" + integer2string(from) + ":]", new_expr, mode);
else
{
auto upper = numeric_cast_v<mp_integer>(to_constant_expr(always.upper()));
auto to = numeric_cast_v<mp_integer>(to_constant_expr(always.to()));
return prefix(
"F[" + integer2string(lower) + ":" + integer2string(upper) + "]",
"F[" + integer2string(from) + ":" + integer2string(to) + "]",
new_expr,
mode);
}
Expand All @@ -188,19 +188,19 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
expr.id() == ID_sva_ranged_s_eventually || expr.id() == ID_sva_eventually)
{
PRECONDITION(mode == PROPERTY);

auto &eventually = to_sva_ranged_predicate_exprt(expr);
auto new_expr = unary_exprt{expr.id(), eventually.op()};
auto lower = numeric_cast_v<mp_integer>(eventually.lower());
auto from = numeric_cast_v<mp_integer>(eventually.from());
if(!eventually.is_range())
return prefix("F[" + integer2string(lower) + "]", new_expr, mode);
return prefix("F[" + integer2string(from) + "]", new_expr, mode);
else if(eventually.is_unbounded())
return prefix("F[" + integer2string(lower) + ":]", new_expr, mode);
return prefix("F[" + integer2string(from) + ":]", new_expr, mode);
else
{
auto upper =
numeric_cast_v<mp_integer>(to_constant_expr(eventually.upper()));
auto to = numeric_cast_v<mp_integer>(to_constant_expr(eventually.to()));
return prefix(
"F[" + integer2string(lower) + ":" + integer2string(upper) + "]",
"F[" + integer2string(from) + ":" + integer2string(to) + "]",
new_expr,
mode);
}
Expand Down
6 changes: 3 additions & 3 deletions src/temporal-logic/nnf.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,14 +79,14 @@ std::optional<exprt> negate_property_node(const exprt &expr)
// not always [x:y] p --> s_eventually [x:y] not p
auto &always = to_sva_ranged_always_expr(expr);
return sva_ranged_s_eventually_exprt{
always.lower(), always.upper(), not_exprt{always.op()}};
always.from(), always.to(), not_exprt{always.op()}};
}
else if(expr.id() == ID_sva_s_always)
{
// not s_always [x:y] p --> eventually [x:y] not p
auto &s_always = to_sva_s_always_expr(expr);
return sva_eventually_exprt{
s_always.lower(), s_always.upper(), not_exprt{s_always.op()}};
s_always.from(), s_always.to(), not_exprt{s_always.op()}};
}
else if(expr.id() == ID_sva_s_eventually)
{
Expand All @@ -98,7 +98,7 @@ std::optional<exprt> negate_property_node(const exprt &expr)
// not eventually[i:j] p --> s_always[i:j] not p
auto &eventually = to_sva_eventually_expr(expr);
return sva_s_always_exprt{
eventually.lower(), eventually.upper(), not_exprt{eventually.op()}};
eventually.from(), eventually.to(), not_exprt{eventually.op()}};
}
else if(expr.id() == ID_sva_until)
{
Expand Down
28 changes: 14 additions & 14 deletions src/temporal-logic/sva_to_ltl.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,28 +57,28 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
if(rec.has_value())
{
// always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());

// Is there an upper end of the range?
if(ranged_always.upper().is_constant())
if(ranged_always.to().is_constant())
{
// upper end set
auto upper_int =
numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.upper()));
PRECONDITION(upper_int >= lower_int);
auto diff = upper_int - lower_int;
auto to_int =
numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.to()));
PRECONDITION(to_int >= from_int);
auto diff = to_int - from_int;

exprt::operandst conjuncts;

for(auto i = 0; i <= diff; i++)
conjuncts.push_back(n_Xes(i, rec.value()));

return n_Xes(lower_int, conjunction(conjuncts));
return n_Xes(from_int, conjunction(conjuncts));
}
else if(ranged_always.upper().id() == ID_infinity)
else if(ranged_always.to().id() == ID_infinity)
{
// always [l:$] op ---> X ... X G op
return n_Xes(lower_int, G_exprt{rec.value()});
return n_Xes(from_int, G_exprt{rec.value()});
}
else
PRECONDITION(false);
Expand All @@ -93,17 +93,17 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
if(rec.has_value())
{
// s_always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
auto upper_int = numeric_cast_v<mp_integer>(ranged_always.upper());
PRECONDITION(upper_int >= lower_int);
auto diff = upper_int - lower_int;
auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());
auto to_int = numeric_cast_v<mp_integer>(ranged_always.to());
PRECONDITION(to_int >= from_int);
auto diff = to_int - from_int;

exprt::operandst conjuncts;

for(auto i = 0; i <= diff; i++)
conjuncts.push_back(n_Xes(i, rec.value()));

return n_Xes(lower_int, conjunction(conjuncts));
return n_Xes(from_int, conjunction(conjuncts));
}
else
return {};
Expand Down
2 changes: 1 addition & 1 deletion src/temporal-logic/trivial_sva.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ exprt trivial_sva(exprt expr)
}
else if(expr.id() == ID_sva_case)
{
expr = to_sva_case_expr(expr).lowering();
expr = to_sva_case_expr(expr).lower();
}

// rewrite the operands, recursively
Expand Down
52 changes: 23 additions & 29 deletions src/trans-word-level/property.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,24 +213,22 @@ static obligationst property_obligations_rec(
const auto &eventually_expr = to_sva_eventually_expr(property_expr);
const auto &op = eventually_expr.op();

mp_integer lower;
if(to_integer_non_constant(eventually_expr.lower(), lower))
throw "failed to convert sva_eventually index";
mp_integer from = numeric_cast_v<mp_integer>(eventually_expr.from());

mp_integer upper;
if(to_integer_non_constant(eventually_expr.upper(), upper))
mp_integer to;
if(to_integer_non_constant(eventually_expr.to(), to))
throw "failed to convert sva_eventually index";

// We rely on NNF.
if(current + lower >= no_timeframes || current + upper >= no_timeframes)
if(current + from >= no_timeframes || current + to >= no_timeframes)
{
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
return obligationst{no_timeframes - 1, true_exprt()};
}

exprt::operandst disjuncts = {};

for(mp_integer u = current + lower; u <= current + upper; ++u)
for(mp_integer u = current + from; u <= current + to; ++u)
{
auto obligations_rec = property_obligations_rec(op, u, no_timeframes);
disjuncts.push_back(obligations_rec.conjunction().second);
Expand Down Expand Up @@ -283,29 +281,24 @@ static obligationst property_obligations_rec(
}
else if(property_expr.id() == ID_sva_ranged_s_eventually)
{
auto &phi = to_sva_ranged_s_eventually_expr(property_expr).op();
auto &lower = to_sva_ranged_s_eventually_expr(property_expr).lower();
auto &upper = to_sva_ranged_s_eventually_expr(property_expr).upper();
const auto &s_eventually = to_sva_ranged_s_eventually_expr(property_expr);
auto from = numeric_cast_v<mp_integer>(s_eventually.from());

auto from_opt = numeric_cast<mp_integer>(lower);
if(!from_opt.has_value())
throw ebmc_errort() << "failed to convert SVA s_eventually from index";

if(*from_opt < 0)
if(from < 0)
throw ebmc_errort() << "SVA s_eventually from index must not be negative";

auto from = std::min(no_timeframes - 1, current + *from_opt);
from = std::min(no_timeframes - 1, current + from);

mp_integer to;

if(upper.id() == ID_infinity)
if(s_eventually.is_unbounded())
{
throw ebmc_errort()
<< "failed to convert SVA s_eventually to index (infinity)";
}
else
{
auto to_opt = numeric_cast<mp_integer>(upper);
auto to_opt = numeric_cast<mp_integer>(s_eventually.to());
if(!to_opt.has_value())
throw ebmc_errort() << "failed to convert SVA s_eventually to index";
to = std::min(current + *to_opt, no_timeframes - 1);
Expand All @@ -316,7 +309,8 @@ static obligationst property_obligations_rec(

for(mp_integer c = from; c <= to; ++c)
{
auto tmp = property_obligations_rec(phi, c, no_timeframes).conjunction();
auto tmp = property_obligations_rec(s_eventually.op(), c, no_timeframes)
.conjunction();
time = std::max(time, tmp.first);
disjuncts.push_back(tmp.second);
}
Expand All @@ -330,14 +324,14 @@ static obligationst property_obligations_rec(
auto &phi = property_expr.id() == ID_sva_ranged_always
? to_sva_ranged_always_expr(property_expr).op()
: to_sva_s_always_expr(property_expr).op();
auto &lower = property_expr.id() == ID_sva_ranged_always
? to_sva_ranged_always_expr(property_expr).lower()
: to_sva_s_always_expr(property_expr).lower();
auto &upper = property_expr.id() == ID_sva_ranged_always
? to_sva_ranged_always_expr(property_expr).upper()
: to_sva_s_always_expr(property_expr).upper();

auto from_opt = numeric_cast<mp_integer>(lower);
auto &from_expr = property_expr.id() == ID_sva_ranged_always
? to_sva_ranged_always_expr(property_expr).from()
: to_sva_s_always_expr(property_expr).from();
auto &to_expr = property_expr.id() == ID_sva_ranged_always
? to_sva_ranged_always_expr(property_expr).to()
: to_sva_s_always_expr(property_expr).to();

auto from_opt = numeric_cast<mp_integer>(from_expr);
if(!from_opt.has_value())
throw ebmc_errort() << "failed to convert SVA always from index";

Expand All @@ -348,13 +342,13 @@ static obligationst property_obligations_rec(

mp_integer to;

if(upper.id() == ID_infinity)
if(to_expr.id() == ID_infinity)
{
to = no_timeframes - 1;
}
else
{
auto to_opt = numeric_cast<mp_integer>(upper);
auto to_opt = numeric_cast<mp_integer>(to_expr);
if(!to_opt.has_value())
throw ebmc_errort() << "failed to convert SVA always to index";
to = std::min(current + *to_opt, no_timeframes - 1);
Expand Down
6 changes: 3 additions & 3 deletions src/verilog/expr2verilog.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -460,11 +460,11 @@ expr2verilogt::resultt expr2verilogt::convert_sva_ranged_predicate(
{
std::string range_str;

range_str = "[" + convert(src.lower()) + ':';
if(src.upper().id() == ID_infinity)
range_str = "[" + convert(src.from()) + ':';
if(src.is_unbounded())
range_str += "$";
else
range_str += convert(src.upper());
range_str += convert(src.to());
range_str += "] ";

auto &src_op = src.op();
Expand Down
4 changes: 2 additions & 2 deletions src/verilog/sva_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ exprt sva_cycle_delay_star_exprt::lower() const
op()};
}

exprt sva_case_exprt::lowering() const
exprt sva_case_exprt::lower() const
{
auto &case_items = this->case_items();

Expand All @@ -51,7 +51,7 @@ exprt sva_case_exprt::lowering() const
reduced.case_items().erase(reduced.case_items().begin());

// rec. call
auto reduced_rec = reduced.lowering();
auto reduced_rec = reduced.lower();

return if_exprt{
disjunction(disjuncts), case_items.front().result(), reduced_rec};
Expand Down
Loading
Loading