Skip to content

extract sva_sequence_matcht #1116

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.

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
May 21, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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/temporal-logic/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ SRC = ctl.cpp \
ltl.cpp \
nnf.cpp \
normalize_property.cpp \
sva_sequence_match.cpp \
sva_to_ltl.cpp \
temporal_logic.cpp \
trivial_sva.cpp \
Expand Down
122 changes: 122 additions & 0 deletions src/temporal-logic/sva_sequence_match.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,122 @@
/*******************************************************************\

Module: SVA Sequence Matches

Author: Daniel Kroening, [email protected]

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

#include "sva_sequence_match.h"

#include <util/arith_tools.h>
#include <util/std_expr.h>

#include <verilog/sva_expr.h>

sva_sequence_matcht sva_sequence_matcht::true_match(const mp_integer &n)
{
sva_sequence_matcht result;
for(mp_integer i; i < n; ++i)
result.cond_vector.push_back(true_exprt{});
return result;
}

// nonoverlapping concatenation
sva_sequence_matcht concat(sva_sequence_matcht a, const sva_sequence_matcht &b)
{
a.cond_vector.insert(
a.cond_vector.end(), b.cond_vector.begin(), b.cond_vector.end());
return a;
}

// overlapping concatenation
sva_sequence_matcht
overlapping_concat(sva_sequence_matcht a, sva_sequence_matcht b)
{
PRECONDITION(!a.empty_match());
PRECONDITION(!b.empty_match());
auto a_last = a.cond_vector.back();
a.cond_vector.pop_back();
b.cond_vector.front() = conjunction({a_last, b.cond_vector.front()});
return concat(std::move(a), b);
}

std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
{
if(sequence.id() == ID_sva_boolean)
{
// atomic proposition
return {sva_sequence_matcht{to_sva_boolean_expr(sequence).op()}};
}
else if(sequence.id() == ID_sva_sequence_concatenation)
{
auto &concatenation = to_sva_sequence_concatenation_expr(sequence);
auto matches_lhs = LTL_sequence_matches(concatenation.lhs());
auto matches_rhs = LTL_sequence_matches(concatenation.rhs());

if(matches_lhs.empty() || matches_rhs.empty())
return {};

std::vector<sva_sequence_matcht> result;

// cross product
for(auto &match_lhs : matches_lhs)
for(auto &match_rhs : matches_rhs)
{
// Sequence concatenation is overlapping
auto new_match = overlapping_concat(match_lhs, match_rhs);
CHECK_RETURN(
new_match.length() == match_lhs.length() + match_rhs.length() - 1);
result.push_back(std::move(new_match));
}
return result;
}
else if(sequence.id() == ID_sva_cycle_delay)
{
auto &delay = to_sva_cycle_delay_expr(sequence);
auto matches = LTL_sequence_matches(delay.op());
auto from_int = numeric_cast_v<mp_integer>(delay.from());

if(matches.empty())
return {};

if(delay.to().is_nil())
{
// delay as instructed
auto delay_sequence = sva_sequence_matcht::true_match(from_int);

for(auto &match : matches)
match = concat(delay_sequence, match);

return matches;
}
else if(delay.to().id() == ID_infinity)
{
return {}; // can't encode
}
else if(delay.to().is_constant())
{
auto to_int = numeric_cast_v<mp_integer>(to_constant_expr(delay.to()));
std::vector<sva_sequence_matcht> new_matches;

for(mp_integer i = from_int; i <= to_int; ++i)
{
// delay as instructed
auto delay_sequence = sva_sequence_matcht::true_match(i);

for(const auto &match : matches)
{
new_matches.push_back(concat(delay_sequence, match));
}
}

return new_matches;
}
else
return {};
}
else
{
return {}; // unsupported
}
}
48 changes: 48 additions & 0 deletions src/temporal-logic/sva_sequence_match.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
/*******************************************************************\

Module: SVA Sequence Matches

Author: Daniel Kroening, [email protected]

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

#ifndef CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H
#define CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H

#include <util/expr.h>
#include <util/mp_arith.h>

// A sequence of match conditions for potential matches of SVA
// sequence expressions.
struct sva_sequence_matcht
{
// the empty match
sva_sequence_matcht()
{
}

// a match of length 1
explicit sva_sequence_matcht(exprt __cond) : cond_vector{1, std::move(__cond)}
{
}

std::vector<exprt> cond_vector;

std::size_t length()
{
return cond_vector.size();
}

bool empty_match() const
{
return cond_vector.empty();
}

// generate true ##1 ... ##1 true with length n
static sva_sequence_matcht true_match(const mp_integer &n);
};

// the set of potential matches for the given sequence expression
std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &);

#endif // CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H
160 changes: 13 additions & 147 deletions src/temporal-logic/sva_to_ltl.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
#include <verilog/sva_expr.h>

#include "ltl.h"
#include "sva_sequence_match.h"
#include "temporal_logic.h"

static exprt n_Xes(mp_integer n, exprt op)
Expand All @@ -22,153 +23,18 @@ static exprt n_Xes(mp_integer n, exprt op)
return n_Xes(n - 1, X_exprt{std::move(op)});
}

// Returns a set of match conditions (given as LTL formula)
struct ltl_sequence_matcht
// c0 ∧ X c1 ∧ XX c2 ....
static exprt ltl(const sva_sequence_matcht &match)
{
// the empty match
ltl_sequence_matcht()
exprt::operandst conjuncts;
conjuncts.reserve(match.cond_vector.size());
for(std::size_t i = 0; i < match.cond_vector.size(); i++)
{
auto &c = match.cond_vector[i];
if(!c.is_true())
conjuncts.push_back(n_Xes(i, c));
}

// a match of length 1
explicit ltl_sequence_matcht(exprt __cond) : cond_vector{1, std::move(__cond)}
{
}

std::vector<exprt> cond_vector;

std::size_t length()
{
return cond_vector.size();
}

bool empty_match() const
{
return cond_vector.empty();
}

// c0 ∧ X c1 ∧ XX c2 ....
exprt cond_expr() const
{
exprt::operandst conjuncts;
conjuncts.reserve(cond_vector.size());
for(std::size_t i = 0; i < cond_vector.size(); i++)
{
auto &c = cond_vector[i];
if(!c.is_true())
conjuncts.push_back(n_Xes(i, c));
}
return conjunction(conjuncts);
}

// generate true ##1 ... ##1 true with length n
static ltl_sequence_matcht true_match(const mp_integer &n)
{
ltl_sequence_matcht result;
for(mp_integer i; i < n; ++i)
result.cond_vector.push_back(true_exprt{});
return result;
}
};

// nonoverlapping concatenation
ltl_sequence_matcht concat(ltl_sequence_matcht a, const ltl_sequence_matcht &b)
{
a.cond_vector.insert(
a.cond_vector.end(), b.cond_vector.begin(), b.cond_vector.end());
return a;
}

// overlapping concatenation
ltl_sequence_matcht
overlapping_concat(ltl_sequence_matcht a, ltl_sequence_matcht b)
{
PRECONDITION(!a.empty_match());
PRECONDITION(!b.empty_match());
auto a_last = a.cond_vector.back();
a.cond_vector.pop_back();
b.cond_vector.front() = conjunction({a_last, b.cond_vector.front()});
return concat(std::move(a), b);
}

std::vector<ltl_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
{
if(sequence.id() == ID_sva_boolean)
{
// atomic proposition
return {ltl_sequence_matcht{to_sva_boolean_expr(sequence).op()}};
}
else if(sequence.id() == ID_sva_sequence_concatenation)
{
auto &concatenation = to_sva_sequence_concatenation_expr(sequence);
auto matches_lhs = LTL_sequence_matches(concatenation.lhs());
auto matches_rhs = LTL_sequence_matches(concatenation.rhs());

if(matches_lhs.empty() || matches_rhs.empty())
return {};

std::vector<ltl_sequence_matcht> result;

// cross product
for(auto &match_lhs : matches_lhs)
for(auto &match_rhs : matches_rhs)
{
// Sequence concatenation is overlapping
auto new_match = overlapping_concat(match_lhs, match_rhs);
CHECK_RETURN(
new_match.length() == match_lhs.length() + match_rhs.length() - 1);
result.push_back(std::move(new_match));
}
return result;
}
else if(sequence.id() == ID_sva_cycle_delay)
{
auto &delay = to_sva_cycle_delay_expr(sequence);
auto matches = LTL_sequence_matches(delay.op());
auto from_int = numeric_cast_v<mp_integer>(delay.from());

if(matches.empty())
return {};

if(delay.to().is_nil())
{
// delay as instructed
auto delay_sequence = ltl_sequence_matcht::true_match(from_int);

for(auto &match : matches)
match = concat(delay_sequence, match);

return matches;
}
else if(delay.to().id() == ID_infinity)
{
return {}; // can't encode
}
else if(delay.to().is_constant())
{
auto to_int = numeric_cast_v<mp_integer>(to_constant_expr(delay.to()));
std::vector<ltl_sequence_matcht> new_matches;

for(mp_integer i = from_int; i <= to_int; ++i)
{
// delay as instructed
auto delay_sequence = ltl_sequence_matcht::true_match(i);

for(const auto &match : matches)
{
new_matches.push_back(concat(delay_sequence, match));
}
}

return new_matches;
}
else
return {};
}
else
{
return {}; // unsupported
}
return conjunction(conjuncts);
}

/// takes an SVA property as input, and returns an equivalent LTL property,
Expand Down Expand Up @@ -296,7 +162,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
{
auto delay = match.length() + (overlapped ? 0 : 1) - 1;
auto delayed_property = n_Xes(delay, property_rec.value());
conjuncts.push_back(implies_exprt{match.cond_expr(), delayed_property});
conjuncts.push_back(implies_exprt{ltl(match), delayed_property});
}
}

Expand Down Expand Up @@ -332,7 +198,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
{
auto delay = match.length() + (overlapped ? 0 : 1) - 1;
auto delayed_property = n_Xes(delay, property_rec.value());
disjuncts.push_back(and_exprt{match.cond_expr(), delayed_property});
disjuncts.push_back(and_exprt{ltl(match), delayed_property});
}
}

Expand Down Expand Up @@ -360,7 +226,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
for(auto &match : matches)
{
if(!match.empty_match())
disjuncts.push_back(match.cond_expr());
disjuncts.push_back(ltl(match));
}

return disjunction(disjuncts);
Expand Down
Loading