diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc index b7d763a4..560a7442 100644 --- a/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc @@ -1,8 +1,8 @@ CORE ../../verilog/SVA/sequence_repetition5.sv --buechi --bound 20 -^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$ -^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$ +^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:9\]\) ##1 main.pulse: PROVED up to bound 20$ +^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:8\]\) ##1 main.pulse: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/empty_sequence1.desc b/regression/verilog/SVA/empty_sequence1.desc index 7aaba5f1..cbb56dc0 100644 --- a/regression/verilog/SVA/empty_sequence1.desc +++ b/regression/verilog/SVA/empty_sequence1.desc @@ -2,7 +2,7 @@ CORE empty_sequence1.sv --bound 5 ^\[main\.p0\] 1 \[\*0\]: REFUTED$ -^\[main\.p1\] 1 \[\*0\] ##1 main\.x == 0: REFUTED$ +^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/sequence_repetition5.desc b/regression/verilog/SVA/sequence_repetition5.desc index aa6cf098..5e4c9489 100644 --- a/regression/verilog/SVA/sequence_repetition5.desc +++ b/regression/verilog/SVA/sequence_repetition5.desc @@ -1,8 +1,8 @@ CORE sequence_repetition5.sv --bound 20 -^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$ -^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$ +^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:9\]\) ##1 main.pulse: PROVED up to bound 20$ +^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:8\]\) ##1 main.pulse: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 399325f7..7276033c 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -60,7 +60,6 @@ IREP_ID_ONE(sva_cycle_delay) IREP_ID_ONE(sva_cycle_delay_star) IREP_ID_ONE(sva_cycle_delay_plus) IREP_ID_ONE(sva_disable_iff) -IREP_ID_ONE(sva_sequence_concatenation) IREP_ID_ONE(sva_sequence_first_match) IREP_ID_ONE(sva_sequence_goto_repetition) IREP_ID_ONE(sva_sequence_intersect) diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp index 89ad35e2..c279d52d 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -327,22 +327,49 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE); return rec(to_sva_boolean_expr(expr).op(), BOOLEAN); } - else if(expr.id() == ID_sva_sequence_concatenation) + else if(expr.id() == ID_sva_cycle_delay) { PRECONDITION(mode == SVA_SEQUENCE); - // SVA sequence concatenation is overlapping, whereas - // the ; operator is nonoverlapping. We special-case - // the following for better readability: - // f ##0 g --> f : g - // 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(expr); + + if(delay.lhs().is_nil()) { - auto &delay = to_sva_cycle_delay_expr(concatenation.rhs()); + auto new_expr = unary_exprt{expr.id(), delay.rhs()}; - auto new_expr = concatenation; - new_expr.rhs() = delay.op(); + if(delay.is_range()) // ##[from:to] rhs + { + auto from = numeric_cast_v(delay.from()); + + if(delay.is_unbounded()) // ##[n:$] rhs + { + return prefix( + "1[*" + integer2string(from) + "..] ; ", new_expr, mode); + } + else + { + auto to = numeric_cast_v(delay.to()); + PRECONDITION(to >= 0); + return prefix( + "1[*" + integer2string(from) + ".." + integer2string(to) + "] ; ", + new_expr, + mode); + } + } + else // ##n rhs + { + auto i = numeric_cast_v(delay.from()); + PRECONDITION(i >= 0); + return prefix("1[*" + integer2string(i) + "] ; ", new_expr, mode); + } + } + else // lhs is not nil + { + // We special-case the following for better readability: + // f ##0 g --> f : g + // f ##1 g --> f ; g + // f ##n g --> f ; 1[*n-1] ; b + auto new_expr = + binary_exprt{delay.lhs(), delay.id(), delay.rhs(), delay.type()}; if(delay.is_range()) { @@ -354,12 +381,12 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) throw ebmc_errort{} << "cannot convert 0.. ranged sequence concatenation to Buechi"; } - else if(delay.is_unbounded()) + else if(delay.is_unbounded()) // f ##[n:$] g { return infix( " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode); } - else + else // f ##[from:to] g { auto to = numeric_cast_v(delay.to()); PRECONDITION(to >= 0); @@ -370,7 +397,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) mode); } } - else + else // f ##n g { auto n = numeric_cast_v(delay.from()); PRECONDITION(n >= 0); @@ -385,39 +412,6 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } } } - else - return infix(":", expr, mode); - } - else if(expr.id() == ID_sva_cycle_delay) - { - PRECONDITION(mode == SVA_SEQUENCE); - auto &delay = to_sva_cycle_delay_expr(expr); - unary_exprt new_expr{expr.id(), delay.op()}; - - if(delay.is_range()) - { - auto from = numeric_cast_v(delay.from()); - - if(delay.is_unbounded()) - { - return prefix("1[*" + integer2string(from) + "..] ; ", new_expr, mode); - } - else - { - auto to = numeric_cast_v(delay.to()); - PRECONDITION(to >= 0); - return prefix( - "1[*" + integer2string(from) + ".." + integer2string(to) + "] ; ", - new_expr, - mode); - } - } - else // singleton - { - auto i = numeric_cast_v(delay.from()); - PRECONDITION(i >= 0); - return prefix("1[*" + integer2string(i) + "] ; ", new_expr, mode); - } } else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something { diff --git a/src/temporal-logic/sva_sequence_match.cpp b/src/temporal-logic/sva_sequence_match.cpp index 54f76610..2bfb614a 100644 --- a/src/temporal-logic/sva_sequence_match.cpp +++ b/src/temporal-logic/sva_sequence_match.cpp @@ -47,7 +47,8 @@ overlapping_concat(sva_sequence_matcht a, sva_sequence_matcht b) 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()}); + if(!a_last.is_true()) + b.cond_vector.front() = conjunction({a_last, b.cond_vector.front()}); return concat(std::move(a), b); } @@ -58,26 +59,6 @@ std::vector LTL_sequence_matches(const exprt &sequence) // 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()); - - std::vector 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_sequence_repetition_star) // [*n], [*n:m] { auto &repetition = to_sva_sequence_repetition_star_expr(sequence); @@ -119,41 +100,61 @@ std::vector LTL_sequence_matches(const exprt &sequence) 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(delay.from()); - if(!delay.is_range()) + // These have an optional LHS and a RHS. + std::vector lhs_matches; + + if(delay.lhs().is_nil()) { - // delay as instructed - auto delay_sequence = sva_sequence_matcht::true_match(from_int); + // If the LHS is not given, it's equivalent to 'true'. + lhs_matches = {sva_sequence_matcht::true_match(1)}; + } + else + { + lhs_matches = LTL_sequence_matches(delay.lhs()); + } - for(auto &match : matches) - match = concat(delay_sequence, match); + // The delay in between lhs and rhs + std::vector delay_matches; + + auto from_int = numeric_cast_v(delay.from()); - return matches; + if(!delay.is_range()) // f ##n g + { + delay_matches = {sva_sequence_matcht::true_match(from_int)}; } - else if(delay.is_unbounded()) + else if(delay.is_unbounded()) // f ##[from:$] g { throw sva_sequence_match_unsupportedt{sequence}; // can't encode } - else + else // f ##[from:to] g { auto to_int = numeric_cast_v(delay.to()); - std::vector new_matches; for(mp_integer i = from_int; i <= to_int; ++i) - { - // delay as instructed - auto delay_sequence = sva_sequence_matcht::true_match(i); + delay_matches.push_back(sva_sequence_matcht::true_match(i)); + } + + // now do RHS + auto rhs_matches = LTL_sequence_matches(delay.rhs()); + + // cross product lhs x delay x rhs + std::vector result; - for(const auto &match : matches) + for(auto &lhs_match : lhs_matches) + for(auto &delay_match : delay_matches) + for(auto &rhs_match : rhs_matches) { - new_matches.push_back(concat(delay_sequence, match)); + // Sequence concatenation is overlapping + auto new_match = + overlapping_concat(lhs_match, concat(delay_match, rhs_match)); + CHECK_RETURN( + new_match.length() == + lhs_match.length() + delay_match.length() + rhs_match.length() - 1); + result.push_back(std::move(new_match)); } - } - return new_matches; - } + return result; } else if(sequence.id() == ID_sva_and) { diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index e61c5342..37141293 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -107,7 +107,6 @@ bool is_SVA_sequence_operator(const exprt &expr) // Note that ID_sva_not does not yield a sequence expression. return id == ID_sva_and || id == ID_sva_or || id == ID_sva_cycle_delay || id == ID_sva_cycle_delay_plus || id == ID_sva_cycle_delay_star || - id == ID_sva_sequence_concatenation || id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match || id == ID_sva_sequence_throughout || id == ID_sva_sequence_within || id == ID_sva_sequence_goto_repetition || diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index 62d5567e..2216f141 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -82,71 +82,76 @@ sequence_matchest instantiate_sequence( const mp_integer &t, const mp_integer &no_timeframes) { + PRECONDITION(t < no_timeframes); + if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something { auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr); - const auto from = numeric_cast_v(sva_cycle_delay_expr.from()); - if(!sva_cycle_delay_expr.is_range()) // ##1 something - { - const auto u = t + from; + // This is the product of the match points on the LHS and RHS, + // with appropriate delay in between. + sequence_matchest lhs_matches; - // Do we exceed the bound? Make it 'false'/'true', depending - // on semantics. - if(u >= no_timeframes) - { - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - if(semantics == sva_sequence_semanticst::WEAK) - return {{no_timeframes - 1, true_exprt{}}}; - else // STRONG - return {}; // no match - } - else - return instantiate_sequence( - sva_cycle_delay_expr.op(), semantics, u, no_timeframes); + if(sva_cycle_delay_expr.lhs().is_nil()) + { + // defaults to a length-1 match with condition 'true' + lhs_matches = {{t, true_exprt{}}}; + } + else + { + lhs_matches = instantiate_sequence( + sva_cycle_delay_expr.lhs(), semantics, t, no_timeframes); } - else // ##[from:to] something + + sequence_matchest result; + + for(auto &lhs_match : lhs_matches) { - auto lower = t + from; - mp_integer upper; + // now delay + const auto from = numeric_cast_v(sva_cycle_delay_expr.from()); - if(sva_cycle_delay_expr.is_unbounded()) + auto t_rhs_from = lhs_match.end_time + from; + mp_integer t_rhs_to; + + if(!sva_cycle_delay_expr.is_range()) // ##1 something + { + t_rhs_to = t_rhs_from; + } + else if(sva_cycle_delay_expr.is_unbounded()) // ##[from:$] something { - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - upper = no_timeframes; + // one beyond the bound + t_rhs_to = no_timeframes; } - else + else // ##[from:to] something { auto to = numeric_cast_v(sva_cycle_delay_expr.to()); - upper = t + to; + t_rhs_to = t_rhs_from + to; } - sequence_matchest matches; - - // Do we exceed the bound? Add an unconditional match when using - // weak semantics. - if(upper >= no_timeframes) + // 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) { - upper = no_timeframes - 1; - - if(semantics == sva_sequence_semanticst::WEAK) + // Do we exceed the bound? + if(t_rhs >= no_timeframes) { - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - matches.emplace_back(no_timeframes - 1, true_exprt()); + if(semantics == sva_sequence_semanticst::WEAK) + result.push_back(lhs_match); } - } + else // still inside bound + { + const auto rhs_matches = instantiate_sequence( + sva_cycle_delay_expr.rhs(), semantics, t_rhs, no_timeframes); - // Add a potential match for each timeframe in the range - for(mp_integer u = lower; u <= upper; ++u) - { - auto sub_result = instantiate_sequence( - sva_cycle_delay_expr.op(), semantics, u, no_timeframes); - for(auto &match : sub_result) - matches.push_back(match); + for(auto &rhs_match : rhs_matches) + { + auto cond = and_exprt{lhs_match.condition(), rhs_match.condition()}; + result.emplace_back(rhs_match.end_time, cond); + } + } } - - return matches; } + + return result; } else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something { @@ -160,42 +165,6 @@ sequence_matchest instantiate_sequence( return instantiate_sequence( cycle_delay_plus.lower(), semantics, t, no_timeframes); } - else if(expr.id() == ID_sva_sequence_concatenation) - { - auto &implication = to_binary_expr(expr); - sequence_matchest result; - - // This is the product of the match points on the LHS and RHS - const auto lhs_matches = - instantiate_sequence(implication.lhs(), semantics, t, no_timeframes); - - for(auto &lhs_match : lhs_matches) - { - auto t_rhs = lhs_match.end_time; - - // Do we exceed the bound? Make it 'false'/'true', depending - // on semantics. - if(t_rhs >= no_timeframes) - { - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - if(semantics == sva_sequence_semanticst::WEAK) - return {{no_timeframes - 1, true_exprt{}}}; - else // STRONG - return {}; // no match - } - - const auto rhs_matches = instantiate_sequence( - implication.rhs(), semantics, t_rhs, no_timeframes); - - for(auto &rhs_match : rhs_matches) - { - auto cond = and_exprt{lhs_match.condition(), rhs_match.condition()}; - result.push_back({rhs_match.end_time, cond}); - } - } - - return result; - } else if(expr.id() == ID_sva_sequence_intersect) { // IEEE 1800-2017 16.9.6 diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index d31d92f7..83f3ef8f 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -141,11 +141,28 @@ Function: expr2verilogt::convert_sva_cycle_delay \*******************************************************************/ -expr2verilogt::resultt expr2verilogt::convert_sva_cycle_delay( - const sva_cycle_delay_exprt &src, - verilog_precedencet precedence) +expr2verilogt::resultt +expr2verilogt::convert_sva_cycle_delay(const sva_cycle_delay_exprt &src) { - std::string dest="##"; + std::string dest; + + if(src.lhs().is_not_nil()) + { + auto lhs = convert_rec(src.lhs()); + if( + lhs.p == verilog_precedencet::MIN && + src.lhs().id() != ID_sva_cycle_delay && + src.lhs().id() != ID_sva_cycle_delay_plus && + src.lhs().id() != ID_sva_cycle_delay_star) + { + dest += "(" + lhs.s + ")"; + } + else + dest += lhs.s; + dest += ' '; + } + + dest += "##"; auto from = convert_rec(src.from()); @@ -163,13 +180,13 @@ expr2verilogt::resultt expr2verilogt::convert_sva_cycle_delay( auto rhs = convert_rec(src.rhs()); - if(precedence > rhs.p) + if(rhs.p == verilog_precedencet::MIN) dest += '('; dest += rhs.s; - if(precedence > rhs.p) + if(rhs.p == verilog_precedencet::MIN) dest += ')'; - return {precedence, dest}; + return {verilog_precedencet::MIN, dest}; } /*******************************************************************\ @@ -214,47 +231,6 @@ expr2verilogt::resultt expr2verilogt::convert_sva_cycle_delay( /*******************************************************************\ -Function: expr2verilogt::convert_sva_sequence_concatenation - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -expr2verilogt::resultt expr2verilogt::convert_sva_sequence_concatenation( - const binary_exprt &src, - verilog_precedencet precedence) -{ - if(src.operands().size()!=2) - return convert_norep(src); - - std::string dest; - - auto op0 = convert_rec(src.op0()); - auto op1 = convert_rec(src.op1()); - - if(precedence > op0.p) - dest += '('; - dest += op0.s; - if(precedence > op0.p) - dest += ')'; - - dest+=' '; - - if(precedence > op0.p) - dest += '('; - dest += op1.s; - if(precedence > op0.p) - dest += ')'; - - return {precedence, dest}; -} - -/*******************************************************************\ - Function: expr2verilogt::convert_sva_sequence_first_match Inputs: @@ -1838,9 +1814,7 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) convert_sva_binary("#=#", to_binary_expr(src)); else if(src.id()==ID_sva_cycle_delay) - return convert_sva_cycle_delay( - to_sva_cycle_delay_expr(src), precedence = verilog_precedencet::MIN); - // not sure about precedence + return convert_sva_cycle_delay(to_sva_cycle_delay_expr(src)); else if(src.id() == ID_sva_strong) return convert_function("strong", src); @@ -1861,11 +1835,6 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) return convert_rec(to_sva_boolean_expr(src).op()); } - else if(src.id()==ID_sva_sequence_concatenation) - return convert_sva_sequence_concatenation( - to_binary_expr(src), precedence = verilog_precedencet::MIN); - // not sure about precedence - else if(src.id() == ID_sva_sequence_first_match) return convert_sva_sequence_first_match( to_sva_sequence_first_match_expr(src)); @@ -1885,16 +1854,6 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) convert_sva_binary("within", to_binary_expr(src)); // not sure about precedence - else if(src.id() == ID_sva_sequence_within) - return convert_sva_sequence_concatenation( - to_binary_expr(src), precedence = verilog_precedencet::MIN); - // not sure about precedence - - else if(src.id() == ID_sva_sequence_throughout) - return convert_sva_sequence_concatenation( - to_binary_expr(src), precedence = verilog_precedencet::MIN); - // not sure about precedence - else if(src.id()==ID_sva_always) return precedence = verilog_precedencet::MIN, convert_sva_unary("always", to_sva_always_expr(src)); diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 32ac685a..1a1a9669 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -156,14 +156,10 @@ class expr2verilogt resultt convert_with(const with_exprt &, verilog_precedencet); - resultt - convert_sva_cycle_delay(const sva_cycle_delay_exprt &, verilog_precedencet); + resultt convert_sva_cycle_delay(const sva_cycle_delay_exprt &); resultt convert_sva_if(const sva_if_exprt &); - resultt - convert_sva_sequence_concatenation(const binary_exprt &, verilog_precedencet); - resultt convert_sva_sequence_first_match(const sva_sequence_first_match_exprt &); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 5206f7f4..8495dc70 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2538,11 +2538,10 @@ property_expr_proper: mto($$, $2); } // requires sequence_expr on the LHS | property_expr cycle_delay_range sequence_expr %prec "##" - { init($$, ID_sva_sequence_concatenation); - mto($$, $1); - stack_expr($2).operands().insert(stack_expr($2).operands().begin(), nil_exprt()); - mto($2, $3); - mto($$, $2); } + { $$=$2; + // preserve the operand ordering as in the source code + stack_expr($$).operands().insert(stack_expr($$).operands().begin(), stack_expr($1)); + mto($$, $3); } // requires sequence_expr on the LHS | '(' property_expr_proper ')' sequence_abbrev { $$ = $4; @@ -2646,11 +2645,10 @@ sequence_expr_proper: stack_expr($$).operands().insert(stack_expr($$).operands().begin(), nil_exprt()); mto($$, $2); } | sequence_expr cycle_delay_range sequence_expr %prec "##" - { init($$, ID_sva_sequence_concatenation); - mto($$, $1); - stack_expr($2).operands().insert(stack_expr($2).operands().begin(), nil_exprt()); - mto($2, $3); - mto($$, $2); } + { $$=$2; + // preserve the operand ordering as in the source code + stack_expr($$).operands().insert(stack_expr($$).operands().begin(), stack_expr($1)); + mto($$, $3); } | '(' sequence_expr_proper ')' { $$ = $2; } | '(' sequence_expr_proper ')' sequence_abbrev diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp index 4f7e5fd3..71fa4f02 100644 --- a/src/verilog/sva_expr.cpp +++ b/src/verilog/sva_expr.cpp @@ -92,10 +92,8 @@ exprt sva_sequence_repetition_star_exprt::lower() const for(; n >= 2; --n) { - auto cycle_delay = - sva_cycle_delay_exprt{from_integer(1, integer_typet{}), op()}; - result = sva_sequence_concatenation_exprt{ - std::move(result), std::move(cycle_delay)}; + result = sva_cycle_delay_exprt{ + std::move(result), from_integer(1, integer_typet{}), nil_exprt{}, op()}; } return result; diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 5d66992e..50cb3537 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -861,35 +861,6 @@ static inline sva_and_exprt &to_sva_and_expr(exprt &expr) return static_cast(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(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(expr); -} - class sva_iff_exprt : public binary_predicate_exprt { public: @@ -1063,16 +1034,6 @@ class sva_cycle_delay_exprt : public exprt return operands()[2].id() == ID_infinity; } - const exprt &op() const - { - return operands()[3]; - } - - exprt &op() - { - return operands()[3]; - } - const exprt &rhs() const { return operands()[3]; diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 52c4a3cb..c97607c1 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -231,7 +231,6 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) return std::move(expr); } else if( - expr.id() == ID_sva_sequence_concatenation || // a ##b c expr.id() == ID_sva_sequence_intersect || expr.id() == ID_sva_sequence_within) { diff --git a/unit/temporal-logic/ltl_sva_to_string.cpp b/unit/temporal-logic/ltl_sva_to_string.cpp index e3dea3de..fb934877 100644 --- a/unit/temporal-logic/ltl_sva_to_string.cpp +++ b/unit/temporal-logic/ltl_sva_to_string.cpp @@ -52,18 +52,16 @@ SCENARIO("Generating a string from a formula") "{1[*1] ; a0}"); REQUIRE( - sequence(sva_sequence_concatenation_exprt{ - p, sva_cycle_delay_exprt{from_integer(0, natural_typet{}), q}}) == - "{a0 : a1}"); + sequence(sva_cycle_delay_exprt{ + p, from_integer(0, natural_typet{}), nil_exprt{}, q}) == "{a0 : a1}"); REQUIRE( - sequence(sva_sequence_concatenation_exprt{ - p, sva_cycle_delay_exprt{from_integer(1, natural_typet{}), q}}) == - "{a0 ; a1}"); + sequence(sva_cycle_delay_exprt{ + p, from_integer(1, natural_typet{}), nil_exprt{}, q}) == "{a0 ; a1}"); REQUIRE( - sequence(sva_sequence_concatenation_exprt{ - p, sva_cycle_delay_exprt{from_integer(10, natural_typet{}), q}}) == + sequence(sva_cycle_delay_exprt{ + p, from_integer(10, natural_typet{}), nil_exprt{}, q}) == "{a0 ; 1[*9] ; a1}"); } }