From 11491fc952151d8e71e4781a2ed12d83055fc3d7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 21 Jun 2025 07:21:09 +0900 Subject: [PATCH] rewrite SVA sequences This adds a facility to rewrite SVA sequences using SVA or such that they do not admit empty matches. This can be used to remove the burden of handling the four cases of possible empty matches in the ##[...] operator from engines that reason about SVA sequences. --- .../sva-buechi/empty_sequence1.bdd.desc | 13 + .../verilog/SVA/empty_sequence1.bdd.desc | 13 + .../verilog/SVA/empty_sequence1.bmc.desc | 2 +- src/temporal-logic/Makefile | 1 + src/temporal-logic/ltl_sva_to_string.cpp | 12 +- src/temporal-logic/rewrite_sva_sequence.cpp | 286 ++++++++++++++++++ src/temporal-logic/rewrite_sva_sequence.h | 22 ++ src/temporal-logic/sva_sequence_match.cpp | 23 +- src/temporal-logic/temporal_logic.cpp | 2 +- src/trans-word-level/sequence.cpp | 86 +++--- src/verilog/sva_expr.cpp | 4 +- src/verilog/sva_expr.h | 12 +- 12 files changed, 418 insertions(+), 58 deletions(-) create mode 100644 regression/ebmc-spot/sva-buechi/empty_sequence1.bdd.desc create mode 100644 regression/verilog/SVA/empty_sequence1.bdd.desc create mode 100644 src/temporal-logic/rewrite_sva_sequence.cpp create mode 100644 src/temporal-logic/rewrite_sva_sequence.h 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)) { } };