diff --git a/regression/verilog/SVA/cover_sequence4.desc b/regression/verilog/SVA/cover_sequence4.desc index 22b36589..d562f38e 100644 --- a/regression/verilog/SVA/cover_sequence4.desc +++ b/regression/verilog/SVA/cover_sequence4.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE cover_sequence4.sv --bound 3 ^\[main\.p0\] cover \(1 \[=10\]\): REFUTED up to bound 3$ @@ -9,4 +9,3 @@ cover_sequence4.sv -- ^warning: ignoring -- -Implementation of [=x:y] is missing. diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index b9341a7d..c8d584ed 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -18,6 +18,63 @@ Author: Daniel Kroening, kroening@kroening.com #include "obligations.h" #include "property.h" +// condition on counters for ocurrences of non-consecutive repetitions +exprt sequence_count_condition( + const sva_sequence_repetition_exprt &expr, + const exprt &counter) +{ + if(expr.is_range()) + { + // number of repetitions inside a range + auto from = numeric_cast_v(expr.from()); + + if(expr.is_unbounded()) + { + return binary_relation_exprt{ + counter, ID_ge, from_integer(from, counter.type())}; + } + else + { + auto to = numeric_cast_v(expr.to()); + + return and_exprt{ + binary_relation_exprt{ + counter, ID_ge, from_integer(from, counter.type())}, + binary_relation_exprt{ + counter, ID_le, from_integer(to, counter.type())}}; + } + } + else + { + // fixed number of repetitions + auto repetitions = numeric_cast_v(expr.repetitions()); + return equal_exprt{counter, from_integer(repetitions, counter.type())}; + } +} + +/// determine type for the repetition counter +typet sequence_count_type( + const sva_sequence_repetition_exprt &expr, + const mp_integer &no_timeframes) +{ + mp_integer max; + + if(expr.is_range()) + { + if(expr.is_unbounded()) + max = numeric_cast_v(expr.from()); + else + max = numeric_cast_v(expr.to()); + } + else + max = numeric_cast_v(expr.repetitions()); + + max = std::max(no_timeframes, max); + + auto bits = address_bits(max + 1); + return unsignedbv_typet{bits}; +} + sequence_matchest instantiate_sequence( exprt expr, sva_sequence_semanticst semantics, @@ -307,7 +364,7 @@ sequence_matchest instantiate_sequence( return result; } - else if(expr.id() == ID_sva_sequence_consecutive_repetition) + else if(expr.id() == ID_sva_sequence_consecutive_repetition) // [*...] { // x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr); @@ -344,69 +401,59 @@ sequence_matchest instantiate_sequence( return result; } - else if(expr.id() == ID_sva_sequence_goto_repetition) + else if(expr.id() == ID_sva_sequence_goto_repetition) // [->...] { - // The 'op' is a Boolean condition, not a sequence. - auto &op = to_sva_sequence_goto_repetition_expr(expr).op(); - auto repetitions_int = numeric_cast_v( - to_sva_sequence_goto_repetition_expr(expr).repetitions()); - PRECONDITION(repetitions_int >= 1); + auto &repetition = to_sva_sequence_goto_repetition_expr(expr); + auto &condition = repetition.op(); sequence_matchest result; // We add up the number of matches of 'op' starting from // timeframe u, until the end of our unwinding. - const auto bits = address_bits(no_timeframes); - const auto zero = from_integer(0, unsignedbv_typet{bits}); - const auto one = from_integer(1, unsignedbv_typet{bits}); - const auto repetitions = from_integer(repetitions_int, zero.type()); + const auto type = sequence_count_type(repetition, no_timeframes); + const auto zero = from_integer(0, type); + const auto one = from_integer(1, type); exprt matches = zero; for(mp_integer u = t; u < no_timeframes; ++u) { // match of op in timeframe u? - auto rec_op = instantiate(op, u, no_timeframes); + auto rec_op = instantiate(condition, u, no_timeframes); // add up matches = plus_exprt{matches, if_exprt{rec_op, one, zero}}; // We have a match for op[->n] if there is a match in timeframe // u and matches is n. - result.emplace_back( - u, and_exprt{rec_op, equal_exprt{matches, repetitions}}); + result.emplace_back(u, sequence_count_condition(repetition, matches)); } return result; } - else if(expr.id() == ID_sva_sequence_non_consecutive_repetition) + else if(expr.id() == ID_sva_sequence_non_consecutive_repetition) // [=...] { - // The 'op' is a Boolean condition, not a sequence. - auto &op = to_sva_sequence_non_consecutive_repetition_expr(expr).op(); - auto repetitions_int = numeric_cast_v( - to_sva_sequence_non_consecutive_repetition_expr(expr).repetitions()); - PRECONDITION(repetitions_int >= 1); + auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr); + auto &condition = repetition.op(); sequence_matchest result; // We add up the number of matches of 'op' starting from // timeframe u, until the end of our unwinding. - const auto bits = - address_bits(std::max(no_timeframes, repetitions_int + 1)); - const auto zero = from_integer(0, unsignedbv_typet{bits}); - const auto one = from_integer(1, zero.type()); - const auto repetitions = from_integer(repetitions_int, zero.type()); + const auto type = sequence_count_type(repetition, no_timeframes); + const auto zero = from_integer(0, type); + const auto one = from_integer(1, type); exprt matches = zero; for(mp_integer u = t; u < no_timeframes; ++u) { // match of op in timeframe u? - auto rec_op = instantiate(op, u, no_timeframes); + auto rec_op = instantiate(condition, u, no_timeframes); // add up matches = plus_exprt{matches, if_exprt{rec_op, one, zero}}; // We have a match for op[=n] if matches is n. - result.emplace_back(u, equal_exprt{matches, repetitions}); + result.emplace_back(u, sequence_count_condition(repetition, matches)); } return result; diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index ba93e737..b4b0aefe 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -608,7 +608,7 @@ expr2verilogt::resultt expr2verilogt::convert_sva_binary( /*******************************************************************\ -Function: expr2verilogt::convert_sva_sequence_consecutive_repetition +Function: expr2verilogt::convert_sva_sequence_repetition Inputs: @@ -622,20 +622,22 @@ expr2verilogt::resultt expr2verilogt::convert_sva_sequence_repetition( const std::string &name, const sva_sequence_repetition_exprt &expr) { - auto op = convert_rec(expr.op()); - if(op.p == verilog_precedencet::MIN) - op.s = "(" + op.s + ")"; + auto op_rec = convert_rec(expr.op()); + + if(op_rec.p == verilog_precedencet::MIN) + op_rec.s = "(" + op_rec.s + ")"; - std::string dest = op.s + " [" + name; + std::string dest = op_rec.s + " [" + name; if(expr.is_range()) { dest += convert_rec(expr.from()).s; + dest += ':'; if(expr.is_unbounded()) - dest += ":$"; + dest += '$'; else - dest += ":" + convert_rec(expr.to()).s; + dest += convert_rec(expr.to()).s; } else dest += convert_rec(expr.repetitions()).s; diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 3a41c2b5..fa03a76f 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -16,8 +16,8 @@ class sva_abort_exprt; class sva_case_exprt; class sva_if_exprt; class sva_ranged_predicate_exprt; -class sva_sequence_repetition_exprt; class sva_sequence_first_match_exprt; +class sva_sequence_repetition_exprt; // Precedences (higher means binds more strongly). // Follows Table 11-2 in IEEE 1800-2017. diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 4abe8adf..fe29b935 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -352,6 +352,9 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr) expr.op1() = from_integer(n, integer_typet{}); + if(expr.op2().is_not_nil()) + convert_expr(expr.op2()); + expr.type() = verilog_sva_sequence_typet{}; return std::move(expr);