Skip to content

BMC: extract instantiate_sequence into separate file #716

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
Sep 23, 2024
Merged

BMC: extract instantiate_sequence into separate file #716

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
1 change: 1 addition & 0 deletions src/trans-word-level/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ SRC = counterexample_word_level.cpp \
property.cpp \
trans_trace_word_level.cpp \
instantiate_word_level.cpp \
sequence.cpp \
show_modules.cpp \
show_module_hierarchy.cpp \
unwind.cpp \
Expand Down
183 changes: 2 additions & 181 deletions src/trans-word-level/instantiate_word_level.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
#include <verilog/sva_expr.h>
#include <verilog/verilog_expr.h>

#include "property.h"
#include "sequence.h"

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

Expand Down Expand Up @@ -91,11 +91,6 @@ class wl_instantiatet
[[nodiscard]] std::pair<mp_integer, exprt>
instantiate_rec(exprt, const mp_integer &t) const;
[[nodiscard]] typet instantiate_rec(typet, const mp_integer &t) const;

// Returns a list of match points and matching conditions
// for the given sequence expression starting at time t
[[nodiscard]] std::vector<std::pair<mp_integer, exprt>>
instantiate_sequence(exprt, const mp_integer &t) const;
};

/*******************************************************************\
Expand All @@ -121,180 +116,6 @@ static exprt default_value(const typet &type)

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

Function: wl_instantiatet::instantiate_sequence

Inputs:

Outputs:

Purpose:

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

std::vector<std::pair<mp_integer, exprt>>
wl_instantiatet::instantiate_sequence(exprt expr, const mp_integer &t) const
{
if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something
{
auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr);

if(sva_cycle_delay_expr.to().is_nil()) // ##1 something
{
mp_integer offset;
if(to_integer_non_constant(sva_cycle_delay_expr.from(), offset))
throw "failed to convert sva_cycle_delay offset";

const auto u = t + offset;

// Do we exceed the bound? Make it 'true'
if(u >= no_timeframes)
{
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
return {{no_timeframes - 1, true_exprt()}};
}
else
return instantiate_sequence(sva_cycle_delay_expr.op(), u);
}
else
{
mp_integer from, to;
if(to_integer_non_constant(sva_cycle_delay_expr.from(), from))
throw "failed to convert sva_cycle_delay offsets";

if(sva_cycle_delay_expr.to().id() == ID_infinity)
{
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
to = no_timeframes - 1;
}
else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to))
throw "failed to convert sva_cycle_delay offsets";

auto lower = t + from;
auto upper = t + to;

// Do we exceed the bound? Make it 'true'
if(upper >= no_timeframes)
{
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
return {{no_timeframes - 1, true_exprt()}};
}

std::vector<std::pair<mp_integer, exprt>> match_points;

for(mp_integer u = lower; u <= upper; ++u)
{
auto sub_result = instantiate_sequence(sva_cycle_delay_expr.op(), u);
for(auto &match_point : sub_result)
match_points.push_back(match_point);
}

return match_points;
}
}
else if(
expr.id() == ID_sva_sequence_concatenation ||
expr.id() == ID_sva_overlapped_implication ||
expr.id() == ID_sva_non_overlapped_implication)
{
auto &implication = to_binary_expr(expr);
std::vector<std::pair<mp_integer, exprt>> result;

// This is the product of the match points on the LHS and RHS
const auto lhs_match_points = instantiate_sequence(implication.lhs(), t);
for(auto &lhs_match_point : lhs_match_points)
{
// The RHS of the non-overlapped implication starts one timeframe later
auto t_rhs = expr.id() == ID_sva_non_overlapped_implication
? lhs_match_point.first + 1
: lhs_match_point.first;

// Do we exceed the bound? Make it 'true'
if(t_rhs >= no_timeframes)
{
DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
return {{no_timeframes - 1, true_exprt()}};
}

const auto rhs_match_points =
instantiate_sequence(implication.rhs(), t_rhs);

for(auto &rhs_match_point : rhs_match_points)
{
exprt cond;
if(expr.id() == ID_sva_sequence_concatenation)
{
cond = and_exprt{lhs_match_point.second, rhs_match_point.second};
}
else if(
expr.id() == ID_sva_overlapped_implication ||
expr.id() == ID_sva_non_overlapped_implication)
{
cond = implies_exprt{lhs_match_point.second, rhs_match_point.second};
}
else
PRECONDITION(false);

result.push_back({rhs_match_point.first, cond});
}
}

return result;
}
else if(expr.id() == ID_sva_sequence_intersect)
{
// IEEE 1800-2017 16.9.6
PRECONDITION(false);
}
else if(expr.id() == ID_sva_sequence_first_match)
{
PRECONDITION(false);
}
else if(expr.id() == ID_sva_sequence_throughout)
{
PRECONDITION(false);
}
else if(expr.id() == ID_sva_sequence_within)
{
PRECONDITION(false);
}
else if(expr.id() == ID_sva_and)
{
// IEEE 1800-2017 16.9.5
// 1. Both operands must match.
// 2. Both sequences start at the same time.
// 3. The end time of the composite sequence is
// the end time of the operand sequence that completes last.
// Condition (3) is TBD.
exprt::operandst conjuncts;

for(auto &op : expr.operands())
conjuncts.push_back(instantiate_rec(op, t).second);

exprt condition = conjunction(conjuncts);
return {{t, condition}};
}
else if(expr.id() == ID_sva_or)
{
// IEEE 1800-2017 16.9.7
// The set of matches of a or b is the set union of the matches of a
// and the matches of b.
std::vector<std::pair<mp_integer, exprt>> result;

for(auto &op : expr.operands())
for(auto &match_point : instantiate_sequence(op, t))
result.push_back(match_point);

return result;
}
else
{
// not a sequence, evaluate as state predicate
return {instantiate_rec(expr, t)};
}
}

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

Function: wl_instantiatet::instantiate_rec

Inputs:
Expand Down Expand Up @@ -324,7 +145,7 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
{
// sequence expressions -- these may have multiple potential
// match points, and evaluate to true if any of them matches
const auto match_points = instantiate_sequence(expr, t);
const auto match_points = instantiate_sequence(expr, t, no_timeframes, ns);
exprt::operandst disjuncts;
disjuncts.reserve(match_points.size());
mp_integer max = t;
Expand Down
Loading