diff --git a/regression/ebmc-spot/sva-buechi/empty_sequence1.bdd.desc b/regression/ebmc-spot/sva-buechi/empty_sequence1.bdd.desc new file mode 100644 index 000000000..de6f1b97d --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/empty_sequence1.bdd.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/empty_sequence1.sv +--buechi --bdd +^\[main\.p0\] 1 \[\*0\]: REFUTED$ +^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED$ +^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED$ +^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$ +^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/empty_sequence1.bdd.desc b/regression/verilog/SVA/empty_sequence1.bdd.desc new file mode 100644 index 000000000..f8bc258e3 --- /dev/null +++ b/regression/verilog/SVA/empty_sequence1.bdd.desc @@ -0,0 +1,13 @@ +CORE +empty_sequence1.sv +--bdd +^\[main\.p0\] 1 \[\*0\]: REFUTED$ +^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: FAILURE: property not supported by BDD engine$ +^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): FAILURE: property not supported by BDD engine$ +^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$ +^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/empty_sequence1.bmc.desc b/regression/verilog/SVA/empty_sequence1.bmc.desc index a9795a05c..0d847a08b 100644 --- a/regression/verilog/SVA/empty_sequence1.bmc.desc +++ b/regression/verilog/SVA/empty_sequence1.bmc.desc @@ -5,7 +5,7 @@ empty_sequence1.sv ^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED up to bound 5$ ^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED up to bound 5$ ^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$ -^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): PROVED up to bound 5$ +^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile index e0bc4dc70..11a251f2a 100644 --- a/src/temporal-logic/Makefile +++ b/src/temporal-logic/Makefile @@ -5,6 +5,7 @@ SRC = ctl.cpp \ ltl_sva_to_string.cpp \ nnf.cpp \ normalize_property.cpp \ + rewrite_sva_sequence.cpp \ sva_sequence_match.cpp \ sva_to_ltl.cpp \ temporal_logic.cpp \ diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp index f0df3e0b5..7e4810421 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, dkr@amazon.com #include #include "ltl.h" +#include "rewrite_sva_sequence.h" #include "temporal_expr.h" #include "temporal_logic.h" @@ -297,9 +298,13 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong) { PRECONDITION(mode == PROPERTY); - // weak closure auto &sequence = to_sva_sequence_property_expr_base(expr).sequence(); - auto op_rec = rec(sequence, SVA_SEQUENCE); + + // re-write to get rid of empty matches + auto sequence_rewritten = rewrite_sva_sequence(sequence); + + auto op_rec = rec(sequence_rewritten, SVA_SEQUENCE); + // weak closure return resultt{precedencet::ATOM, '{' + op_rec.s + '}'}; } else if(expr.id() == ID_sva_or) @@ -446,7 +451,8 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } else if(repetition.is_empty_match()) { - throw ltl_sva_to_string_unsupportedt{expr}; + // handled by rewite_sva_sequence + return resultt{precedencet::ATOM, "0"}; } else if(repetition.is_singleton()) { diff --git a/src/temporal-logic/rewrite_sva_sequence.cpp b/src/temporal-logic/rewrite_sva_sequence.cpp new file mode 100644 index 000000000..15b889bda --- /dev/null +++ b/src/temporal-logic/rewrite_sva_sequence.cpp @@ -0,0 +1,286 @@ +/*******************************************************************\ + +Module: Rewrite SVA Sequences + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "rewrite_sva_sequence.h" + +#include +#include + +#include + +#include "temporal_logic.h" + +/// 1800-2017 F.4.3 +/// Returns true iff the given SVA sequence admits an empty match. +bool admits_empty(const exprt &expr) +{ + PRECONDITION(expr.type().id() == ID_verilog_sva_sequence); + PRECONDITION(is_SVA_sequence_operator(expr)); + + if(expr.id() == ID_sva_boolean) + return false; // admits_empty(b) = 0 + else if(expr.id() == ID_sva_cycle_delay) + { + auto &cycle_delay = to_sva_cycle_delay_expr(expr); + + if(cycle_delay.from().is_zero() && !cycle_delay.is_range()) + { + // admits_empty((r1 ##0 r2)) = 0 + return false; + } + else + { + // admits_empty((r1 ##1 r2)) = admits_empty(r1) && admits_empty(r2) + return cycle_delay.lhs().is_not_nil() && + admits_empty(cycle_delay.lhs()) && admits_empty(cycle_delay.rhs()); + } + } + else if(expr.id() == ID_sva_cycle_delay_star) + { + auto &cycle_delay = to_sva_cycle_delay_star_expr(expr); + + return cycle_delay.lhs().is_not_nil() && admits_empty(cycle_delay.lhs()) && + admits_empty(cycle_delay.rhs()); + } + else if(expr.id() == ID_sva_cycle_delay_plus) + { + auto &cycle_delay = to_sva_cycle_delay_plus_expr(expr); + + return cycle_delay.lhs().is_not_nil() && admits_empty(cycle_delay.lhs()) && + admits_empty(cycle_delay.rhs()); + } + else if(expr.id() == ID_sva_or) + { + // admits_empty((r1 or r2)) = admits_empty(r1) || admits_empty(r2) + auto &or_expr = to_sva_or_expr(expr); + return admits_empty(or_expr.lhs()) || admits_empty(or_expr.rhs()); + } + else if(expr.id() == ID_sva_sequence_intersect) + { + // admits_empty((r1 intersect r2)) = admits_empty(r1) && admits_empty(r2) + auto &intersect_expr = to_sva_sequence_intersect_expr(expr); + return admits_empty(intersect_expr.lhs()) && + admits_empty(intersect_expr.rhs()); + } + else if(expr.id() == ID_sva_sequence_first_match) + { + // admits_empty(first_match(r)) = admits_empty(r) + auto &first_match_expr = to_sva_sequence_first_match_expr(expr); + return admits_empty(first_match_expr.lhs()) && + admits_empty(first_match_expr.rhs()); + } + else if(expr.id() == ID_sva_sequence_repetition_star) + { + // admits_empty(r[*0]) = 1 + // admits_empty(r[*1:$]) = admits_empty(r) + auto &repetition_expr = to_sva_sequence_repetition_star_expr(expr); + if(repetition_expr.is_range()) + { + if(repetition_expr.from().is_zero()) + return true; + else + return admits_empty(repetition_expr.op()); + } + else // singleton + { + if(repetition_expr.repetitions().is_zero()) + return true; + else + return admits_empty(repetition_expr.op()); + } + } + else if( + expr.id() == ID_sva_sequence_goto_repetition || + expr.id() == ID_sva_sequence_non_consecutive_repetition) + { + return false; + } + else + { + DATA_INVARIANT(false, "unexpected SVA sequence: " + expr.id_string()); + } +} + +exprt rewrite_sva_sequence(exprt expr) +{ + PRECONDITION(expr.type().id() == ID_verilog_sva_sequence); + PRECONDITION(is_SVA_sequence_operator(expr)); + + if(expr.id() == ID_sva_cycle_delay) + { + // 1800-2017 16.9.2.1 + // - (empty ##0 seq) does not result in a match. + // - (seq ##0 empty) does not result in a match. + // - (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq). + // - (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true). + auto &cycle_delay_expr = to_sva_cycle_delay_expr(expr); + + bool lhs_admits_empty = cycle_delay_expr.lhs().is_not_nil() && + admits_empty(cycle_delay_expr.lhs()); + + bool rhs_admits_empty = admits_empty(cycle_delay_expr.rhs()); + + // apply recursively to operands + if(cycle_delay_expr.lhs().is_not_nil()) + cycle_delay_expr.lhs() = rewrite_sva_sequence(cycle_delay_expr.lhs()); + + cycle_delay_expr.rhs() = rewrite_sva_sequence(cycle_delay_expr.rhs()); + + // consider empty match cases + if(!lhs_admits_empty && !rhs_admits_empty) + return cycle_delay_expr; + + if(lhs_admits_empty) + { + if(cycle_delay_expr.is_range()) + { + mp_integer from_int = + numeric_cast_v(cycle_delay_expr.from()); + DATA_INVARIANT(from_int >= 0, "delay must not be negative"); + abort(); + } + else // singleton + { + mp_integer delay_int = + numeric_cast_v(cycle_delay_expr.from()); + DATA_INVARIANT(delay_int >= 0, "delay must not be negative"); + + // lhs ##0 rhs + if(delay_int == 0) + return cycle_delay_expr; + else + { + // (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq). + auto delay = + from_integer(delay_int - 1, cycle_delay_expr.from().type()); + auto empty_match_case = + sva_cycle_delay_exprt{delay, cycle_delay_expr.rhs()}; + return sva_or_exprt{empty_match_case, cycle_delay_expr, expr.type()}; + } + } + } + else if(rhs_admits_empty) + { + if(cycle_delay_expr.is_range()) + { + mp_integer from_int = + numeric_cast_v(cycle_delay_expr.from()); + DATA_INVARIANT(from_int >= 0, "delay must not be negative"); + abort(); + } + else // singleton + { + mp_integer delay_int = + numeric_cast_v(cycle_delay_expr.from()); + DATA_INVARIANT(delay_int >= 0, "delay must not be negative"); + + // lhs ##0 rhs + if(delay_int == 0) + return cycle_delay_expr; + else + { + // (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true). + auto delay = + from_integer(delay_int - 1, cycle_delay_expr.from().type()); + auto empty_match_case = sva_cycle_delay_exprt{ + cycle_delay_expr.lhs(), + delay, + nil_exprt{}, + sva_boolean_exprt{true_exprt{}, expr.type()}}; + return sva_or_exprt{empty_match_case, cycle_delay_expr, expr.type()}; + } + } + } + else // neither lhs nor rhs admit an empty match + return cycle_delay_expr; + } + else if(expr.id() == ID_sva_sequence_repetition_star) + { + auto &repetition_expr = to_sva_sequence_repetition_star_expr(expr); + repetition_expr.op() = rewrite_sva_sequence(repetition_expr.op()); + + if(repetition_expr.is_empty_match()) + { + // Empty match. Leave as is. Now denotes "no match". + } + else if(!repetition_expr.repetitions_given()) + { + // f [*] g ---> f [*1:$] g + repetition_expr = sva_sequence_repetition_star_exprt{ + repetition_expr.op(), + from_integer(1, integer_typet{}), + infinity_exprt{integer_typet{}}}; + } + else if(repetition_expr.is_range() && repetition_expr.from().is_zero()) + { + // f [*0:x] g ---> f [*1:x] g + repetition_expr.from() = from_integer(1, repetition_expr.from().type()); + } + + return repetition_expr; + } + else if(expr.id() == ID_sva_sequence_repetition_plus) + { + auto &repetition_expr = to_sva_sequence_repetition_plus_expr(expr); + repetition_expr.op() = rewrite_sva_sequence(repetition_expr.op()); + return repetition_expr; + } + else if( + expr.id() == ID_sva_or || expr.id() == ID_sva_and || + expr.id() == ID_sva_sequence_intersect || + expr.id() == ID_sva_sequence_within) + { + // All operands are sequences + for(auto &op : expr.operands()) + op = rewrite_sva_sequence(op); + return expr; + } + else if(expr.id() == ID_sva_sequence_first_match) + { + auto &first_match = to_sva_sequence_first_match_expr(expr); + first_match.sequence() = rewrite_sva_sequence(first_match.sequence()); + return first_match; + } + else if(expr.id() == ID_sva_cycle_delay_star) + { + auto &cycle_delay = to_sva_cycle_delay_star_expr(expr); + if(cycle_delay.lhs().is_not_nil()) + cycle_delay.lhs() = rewrite_sva_sequence(cycle_delay.lhs()); + cycle_delay.rhs() = rewrite_sva_sequence(cycle_delay.rhs()); + return expr; + } + else if(expr.id() == ID_sva_cycle_delay_plus) + { + auto &cycle_delay = to_sva_cycle_delay_plus_expr(expr); + if(cycle_delay.lhs().is_not_nil()) + cycle_delay.lhs() = rewrite_sva_sequence(cycle_delay.lhs()); + cycle_delay.rhs() = rewrite_sva_sequence(cycle_delay.rhs()); + return expr; + } + else if(expr.id() == ID_sva_sequence_throughout) + { + auto &throughout = to_sva_sequence_throughout_expr(expr); + throughout.sequence() = rewrite_sva_sequence(throughout.sequence()); + return expr; + } + else if( + expr.id() == ID_sva_sequence_goto_repetition || + expr.id() == ID_sva_sequence_non_consecutive_repetition) + { + // these take a Boolean as argument, not a sequence + return expr; + } + else if(expr.id() == ID_sva_boolean) + { + return expr; + } + else + { + DATA_INVARIANT(false, "unexpected SVA sequence: " + expr.id_string()); + } +} diff --git a/src/temporal-logic/rewrite_sva_sequence.h b/src/temporal-logic/rewrite_sva_sequence.h new file mode 100644 index 000000000..c5ebf84fc --- /dev/null +++ b/src/temporal-logic/rewrite_sva_sequence.h @@ -0,0 +1,22 @@ +/*******************************************************************\ + +Module: Rewrite SVA Sequences + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_TEMPORAL_LOGICS_REWRITE_SVA_SEQUENCE_H +#define CPROVER_TEMPORAL_LOGICS_REWRITE_SVA_SEQUENCE_H + +#include + +/// 1800-2017 F.4.3 +/// Returns true iff the given SVA sequence admits an empty match. +bool admits_empty(const exprt &); + +/// Implements the rewriting rules in 1800-2017 16.9.2.1. +/// The resulting sequence expression do not admit empty matches. +exprt rewrite_sva_sequence(exprt); + +#endif // CPROVER_TEMPORAL_LOGICS_REWRITE_SVA_SEQUENCE_H diff --git a/src/temporal-logic/sva_sequence_match.cpp b/src/temporal-logic/sva_sequence_match.cpp index f28154e5b..61d58efed 100644 --- a/src/temporal-logic/sva_sequence_match.cpp +++ b/src/temporal-logic/sva_sequence_match.cpp @@ -13,6 +13,8 @@ Author: Daniel Kroening, dkr@amazon.com #include +#include "rewrite_sva_sequence.h" + sva_sequence_matcht sva_sequence_matcht::true_match(const mp_integer &n) { auto n_size_t = numeric_cast_v(n); @@ -51,7 +53,7 @@ overlapping_concat(sva_sequence_matcht a, sva_sequence_matcht b) return concat(std::move(a), b); } -std::vector LTL_sequence_matches(const exprt &sequence) +std::vector sva_sequence_matches_rec(const exprt &sequence) { if(sequence.id() == ID_sva_boolean) { @@ -61,7 +63,7 @@ std::vector LTL_sequence_matches(const exprt &sequence) else if(sequence.id() == ID_sva_sequence_repetition_star) // [*n], [*n:m] { auto &repetition = to_sva_sequence_repetition_star_expr(sequence); - auto matches_op = LTL_sequence_matches(repetition.op()); + auto matches_op = sva_sequence_matches_rec(repetition.op()); std::vector result; @@ -144,6 +146,10 @@ std::vector LTL_sequence_matches(const exprt &sequence) for(auto &delay_match : delay_matches) for(auto &rhs_match : rhs_matches) { + // Drop empty matches, taken care of by rewrite_sva_sequence + if(lhs_match.empty_match() || rhs_match.empty_match()) + continue; + // Sequence concatenation is overlapping auto new_match = overlapping_concat(lhs_match, concat(delay_match, rhs_match)); @@ -163,8 +169,8 @@ std::vector LTL_sequence_matches(const exprt &sequence) // 3. The end time of the composite sequence is // the end time of the operand sequence that completes last. auto &and_expr = to_sva_and_expr(sequence); - auto matches_lhs = LTL_sequence_matches(and_expr.lhs()); - auto matches_rhs = LTL_sequence_matches(and_expr.rhs()); + auto matches_lhs = sva_sequence_matches_rec(and_expr.lhs()); + auto matches_rhs = sva_sequence_matches_rec(and_expr.rhs()); std::vector result; @@ -200,7 +206,7 @@ std::vector LTL_sequence_matches(const exprt &sequence) for(auto &op : to_sva_or_expr(sequence).operands()) { - auto op_matches = LTL_sequence_matches(op); + auto op_matches = sva_sequence_matches_rec(op); if(op_matches.empty()) throw sva_sequence_match_unsupportedt{sequence}; // not supported for(auto &match : op_matches) @@ -214,3 +220,10 @@ std::vector LTL_sequence_matches(const exprt &sequence) throw sva_sequence_match_unsupportedt{sequence}; // not supported } } + +std::vector LTL_sequence_matches(const exprt &sequence) +{ + // rewrite, then do recursion + auto rewritten = rewrite_sva_sequence(sequence); + return sva_sequence_matches_rec(rewritten); +} diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 371412932..a93d55d63 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -112,7 +112,7 @@ bool is_SVA_sequence_operator(const exprt &expr) id == ID_sva_sequence_goto_repetition || id == ID_sva_sequence_non_consecutive_repetition || id == ID_sva_sequence_repetition_star || - id == ID_sva_sequence_repetition_plus; + id == ID_sva_sequence_repetition_plus || id == ID_sva_boolean; } bool is_SVA_operator(const exprt &expr) diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index 04d3aa49a..cdb590c22 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -76,7 +77,7 @@ typet sequence_count_type( return unsignedbv_typet{bits}; } -sequence_matchest instantiate_sequence( +sequence_matchest instantiate_sequence_rec( exprt expr, sva_sequence_semanticst semantics, const mp_integer &t, @@ -99,7 +100,7 @@ sequence_matchest instantiate_sequence( } else { - lhs_matches = instantiate_sequence( + lhs_matches = instantiate_sequence_rec( sva_cycle_delay_expr.lhs(), semantics, t, no_timeframes); } @@ -107,6 +108,9 @@ sequence_matchest instantiate_sequence( for(auto &lhs_match : lhs_matches) { + if(lhs_match.empty_match()) + continue; // handled by rewrite_sva_sequence + // now delay const auto from = numeric_cast_v(sva_cycle_delay_expr.from()); DATA_INVARIANT(from >= 0, "##n must not be negative"); @@ -129,24 +133,6 @@ sequence_matchest instantiate_sequence( t_rhs_to = t_rhs_from + to; } - // Implement 1800-2017 16.9.2.1 - if(lhs_match.empty_match()) - { - if(from == 0) - { - // (empty ##0 seq) does not result in a match. - continue; - } - else - { - // (empty ##n seq), where n is greater than 0, - // is equivalent to (##(n-1) seq). - t_rhs_from = t_rhs_from - 1; - if(t_rhs_to != no_timeframes) - t_rhs_to = t_rhs_to - 1; - } - } - // Add a potential match for each timeframe in the range for(mp_integer t_rhs = t_rhs_from; t_rhs <= t_rhs_to; ++t_rhs) { @@ -158,13 +144,18 @@ sequence_matchest instantiate_sequence( } else // still inside bound { - const auto rhs_matches = instantiate_sequence( + const auto rhs_matches = instantiate_sequence_rec( sva_cycle_delay_expr.rhs(), semantics, t_rhs, no_timeframes); for(auto &rhs_match : rhs_matches) { - auto cond = and_exprt{lhs_match.condition(), rhs_match.condition()}; - result.emplace_back(rhs_match.end_time, cond); + // empty matches are handled by rewrite_sva_sequence + if(!rhs_match.empty_match()) + { + auto cond = + and_exprt{lhs_match.condition(), rhs_match.condition()}; + result.emplace_back(rhs_match.end_time, cond); + } } } } @@ -175,13 +166,13 @@ sequence_matchest instantiate_sequence( else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something { auto &cycle_delay_star = to_sva_cycle_delay_star_expr(expr); - return instantiate_sequence( + return instantiate_sequence_rec( cycle_delay_star.lower(), semantics, t, no_timeframes); } else if(expr.id() == ID_sva_cycle_delay_plus) // ##[+] something { auto &cycle_delay_plus = to_sva_cycle_delay_plus_expr(expr); - return instantiate_sequence( + return instantiate_sequence_rec( cycle_delay_plus.lower(), semantics, t, no_timeframes); } else if(expr.id() == ID_sva_sequence_intersect) @@ -194,9 +185,9 @@ sequence_matchest instantiate_sequence( auto &intersect = to_sva_sequence_intersect_expr(expr); const auto lhs_matches = - instantiate_sequence(intersect.lhs(), semantics, t, no_timeframes); + instantiate_sequence_rec(intersect.lhs(), semantics, t, no_timeframes); const auto rhs_matches = - instantiate_sequence(intersect.rhs(), semantics, t, no_timeframes); + instantiate_sequence_rec(intersect.rhs(), semantics, t, no_timeframes); sequence_matchest result; @@ -220,8 +211,8 @@ sequence_matchest instantiate_sequence( { auto &first_match = to_sva_sequence_first_match_expr(expr); - const auto matches = - instantiate_sequence(first_match.sequence(), semantics, t, no_timeframes); + const auto matches = instantiate_sequence_rec( + first_match.sequence(), semantics, t, no_timeframes); // the match of seq with the earliest ending clock tick is a // match of first_match (seq) @@ -257,8 +248,8 @@ sequence_matchest instantiate_sequence( // - exp evaluates to true at each clock tick of the interval. auto &throughout = to_sva_sequence_throughout_expr(expr); - const auto matches = - instantiate_sequence(throughout.sequence(), semantics, t, no_timeframes); + const auto matches = instantiate_sequence_rec( + throughout.sequence(), semantics, t, no_timeframes); sequence_matchest result; @@ -285,7 +276,7 @@ sequence_matchest instantiate_sequence( auto &within_expr = to_sva_sequence_within_expr(expr); const auto matches_rhs = - instantiate_sequence(within_expr.rhs(), semantics, t, no_timeframes); + instantiate_sequence_rec(within_expr.rhs(), semantics, t, no_timeframes); sequence_matchest result; @@ -293,7 +284,7 @@ sequence_matchest instantiate_sequence( { for(auto start_lhs = t; start_lhs <= match_rhs.end_time; ++start_lhs) { - auto matches_lhs = instantiate_sequence( + auto matches_lhs = instantiate_sequence_rec( within_expr.lhs(), semantics, start_lhs, no_timeframes); for(auto &match_lhs : matches_lhs) @@ -321,9 +312,9 @@ sequence_matchest instantiate_sequence( // the end time of the operand sequence that completes last. auto &and_expr = to_sva_and_expr(expr); auto matches_lhs = - instantiate_sequence(and_expr.lhs(), semantics, t, no_timeframes); + instantiate_sequence_rec(and_expr.lhs(), semantics, t, no_timeframes); auto matches_rhs = - instantiate_sequence(and_expr.rhs(), semantics, t, no_timeframes); + instantiate_sequence_rec(and_expr.rhs(), semantics, t, no_timeframes); sequence_matchest result; @@ -345,8 +336,11 @@ sequence_matchest instantiate_sequence( sequence_matchest result; for(auto &op : expr.operands()) - for(auto &match : instantiate_sequence(op, semantics, t, no_timeframes)) + for(auto &match : + instantiate_sequence_rec(op, semantics, t, no_timeframes)) + { result.push_back(match); + } return result; } @@ -355,31 +349,31 @@ sequence_matchest instantiate_sequence( auto &repetition = to_sva_sequence_repetition_star_expr(expr); if(repetition.is_empty_match()) { - // [*0] denotes the empty match + // [*0] denotes the empty match. return {sequence_matcht::empty_match(t)}; } else if(repetition.is_unbounded() && repetition.repetitions_given()) { - // [*from:$] -> op[*from:to] + // op[*from:$] -> op[*from:to] // with to = no_timeframes - t auto to = from_integer(no_timeframes - t, integer_typet{}); auto new_repetition = sva_sequence_repetition_star_exprt{ repetition.op(), repetition.from(), to}; - return instantiate_sequence( + return instantiate_sequence_rec( new_repetition.lower(), semantics, t, no_timeframes); } else { // [*], [*n], [*x:y] - return instantiate_sequence( + return instantiate_sequence_rec( repetition.lower(), semantics, t, no_timeframes); } } else if(expr.id() == ID_sva_sequence_repetition_plus) // [+] { auto &repetition = to_sva_sequence_repetition_plus_expr(expr); - return instantiate_sequence( + return instantiate_sequence_rec( repetition.lower(), semantics, t, no_timeframes); } else if(expr.id() == ID_sva_sequence_goto_repetition) // [->...] @@ -452,3 +446,13 @@ sequence_matchest instantiate_sequence( false, "unexpected sequence expression", expr.pretty()); } } + +sequence_matchest instantiate_sequence( + exprt expr, + sva_sequence_semanticst semantics, + const mp_integer &t, + const mp_integer &no_timeframes) +{ + auto rewritten = rewrite_sva_sequence(expr); + return instantiate_sequence_rec(rewritten, semantics, t, no_timeframes); +} diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp index 71fa4f02c..223ab386d 100644 --- a/src/verilog/sva_expr.cpp +++ b/src/verilog/sva_expr.cpp @@ -118,7 +118,9 @@ exprt sva_sequence_repetition_star_exprt::lower() const { auto n_expr = from_integer(n, integer_typet{}); result = sva_or_exprt{ - std::move(result), sva_sequence_repetition_star_exprt{op(), n_expr}}; + std::move(result), + sva_sequence_repetition_star_exprt{op(), n_expr}, + verilog_sva_sequence_typet{}}; } return result; diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index d86c2bfd3..9b3f68a2e 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -838,11 +838,11 @@ static inline sva_not_exprt &to_sva_not_expr(exprt &expr) return static_cast(expr); } -class sva_and_exprt : public binary_predicate_exprt +class sva_and_exprt : public binary_exprt { public: - explicit sva_and_exprt(exprt op0, exprt op1) - : binary_predicate_exprt(std::move(op0), ID_sva_and, std::move(op1)) + explicit sva_and_exprt(exprt op0, exprt op1, typet type) + : binary_exprt(std::move(op0), ID_sva_and, std::move(op1), std::move(type)) { } }; @@ -907,11 +907,11 @@ static inline sva_implies_exprt &to_sva_implies_expr(exprt &expr) return static_cast(expr); } -class sva_or_exprt : public binary_predicate_exprt +class sva_or_exprt : public binary_exprt { public: - explicit sva_or_exprt(exprt op0, exprt op1) - : binary_predicate_exprt(std::move(op0), ID_sva_or, std::move(op1)) + explicit sva_or_exprt(exprt op0, exprt op1, typet type) + : binary_exprt(std::move(op0), ID_sva_or, std::move(op1), std::move(type)) { } };