Skip to content

SVA: strengthen typing of sva_sequence_concatenation_exprt #1161

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

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

SVA: strengthen typing of sva_sequence_concatenation_exprt #1161

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
76 changes: 35 additions & 41 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 @@ -337,56 +337,50 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
// f ##1 g --> f ; g
// f ##n g --> f ; 1[*n-1] ; b
auto &concatenation = to_sva_sequence_concatenation_expr(expr);
if(concatenation.rhs().id() == ID_sva_cycle_delay)
{
auto &delay = to_sva_cycle_delay_expr(concatenation.rhs());
auto &delay = concatenation.rhs();

auto new_expr = concatenation;
new_expr.rhs() = delay.op();
binary_exprt new_expr = concatenation;
new_expr.rhs() = delay.op();

if(delay.is_range())
{
auto from = numeric_cast_v<mp_integer>(delay.from());
if(delay.is_range())
{
auto from = numeric_cast_v<mp_integer>(delay.from());

if(from == 0)
{
// requires treatment of empty sequences on lhs
throw ebmc_errort{}
<< "cannot convert 0.. ranged sequence concatenation to Buechi";
}
else if(delay.is_unbounded())
{
return infix(
" ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode);
}
else
{
auto to = numeric_cast_v<mp_integer>(delay.to());
PRECONDITION(to >= 0);
return infix(
" ; 1[*" + integer2string(from - 1) + ".." +
integer2string(to - 1) + "] ; ",
new_expr,
mode);
}
if(from == 0)
{
// requires treatment of empty sequences on lhs
throw ebmc_errort{}
<< "cannot convert 0.. ranged sequence concatenation to Buechi";
}
else if(delay.is_unbounded())
{
return infix(
" ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode);
}
else
{
auto n = numeric_cast_v<mp_integer>(delay.from());
PRECONDITION(n >= 0);
if(n == 0)
return infix(" : ", new_expr, mode);
else if(n == 1)
return infix(" ; ", new_expr, mode);
else
{
return infix(
" ; 1[*" + integer2string(n - 1) + "] ; ", new_expr, mode);
}
auto to = numeric_cast_v<mp_integer>(delay.to());
PRECONDITION(to >= 0);
return infix(
" ; 1[*" + integer2string(from - 1) + ".." + integer2string(to - 1) +
"] ; ",
new_expr,
mode);
}
}
else
return infix(":", expr, mode);
{
auto n = numeric_cast_v<mp_integer>(delay.from());
PRECONDITION(n >= 0);
if(n == 0)
return infix(" : ", new_expr, mode);
else if(n == 1)
return infix(" ; ", new_expr, mode);
else
{
return infix(" ; 1[*" + integer2string(n - 1) + "] ; ", new_expr, mode);
}
}
}
else if(expr.id() == ID_sva_cycle_delay)
{
Expand Down
71 changes: 42 additions & 29 deletions src/verilog/sva_expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -861,35 +861,6 @@ static inline sva_and_exprt &to_sva_and_expr(exprt &expr)
return static_cast<sva_and_exprt &>(expr);
}

class sva_sequence_concatenation_exprt : public binary_exprt
{
public:
explicit sva_sequence_concatenation_exprt(exprt op0, exprt op1)
: binary_exprt(
std::move(op0),
ID_sva_sequence_concatenation,
std::move(op1),
verilog_sva_sequence_typet{})
{
}
};

static inline const sva_sequence_concatenation_exprt &
to_sva_sequence_concatenation_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
return static_cast<const sva_sequence_concatenation_exprt &>(expr);
}

static inline sva_sequence_concatenation_exprt &
to_sva_sequence_concatenation_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
return static_cast<sva_sequence_concatenation_exprt &>(expr);
}

class sva_iff_exprt : public binary_predicate_exprt
{
public:
Expand Down Expand Up @@ -1084,6 +1055,48 @@ static inline sva_cycle_delay_exprt &to_sva_cycle_delay_expr(exprt &expr)
return static_cast<sva_cycle_delay_exprt &>(expr);
}

class sva_sequence_concatenation_exprt : public binary_exprt
{
public:
// The lhs is a sequence, the rhs is a sva_cycle_delay expression
explicit sva_sequence_concatenation_exprt(
exprt __lhs,
sva_cycle_delay_exprt __rhs)
: binary_exprt(
std::move(__lhs),
ID_sva_sequence_concatenation,
std::move(__rhs),
verilog_sva_sequence_typet{})
{
}

const sva_cycle_delay_exprt &rhs() const
{
return static_cast<const sva_cycle_delay_exprt &>(binary_exprt::rhs());
}

sva_cycle_delay_exprt &rhs()
{
return static_cast<sva_cycle_delay_exprt &>(binary_exprt::rhs());
}
};

static inline const sva_sequence_concatenation_exprt &
to_sva_sequence_concatenation_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
return static_cast<const sva_sequence_concatenation_exprt &>(expr);
}

static inline sva_sequence_concatenation_exprt &
to_sva_sequence_concatenation_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
return static_cast<sva_sequence_concatenation_exprt &>(expr);
}

class sva_cycle_delay_plus_exprt : public unary_exprt
{
public:
Expand Down
Loading