diff --git a/regression/verilog/SVA/cover_sequence2.desc b/regression/verilog/SVA/cover_sequence2.desc index 8336bbb5..5ddfb9ce 100644 --- a/regression/verilog/SVA/cover_sequence2.desc +++ b/regression/verilog/SVA/cover_sequence2.desc @@ -1,11 +1,12 @@ -KNOWNBUG +CORE cover_sequence2.sv ---bound 2 -^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): PROVED$ -^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 2$ +--bound 5 +^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): REFUTED up to bound 5$ +^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 5$ +^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): PROVED$ +^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): REFUTED up to bound 5$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -Cover property p0 cannot ever hold, but is shown proven when using a small bound. diff --git a/regression/verilog/SVA/cover_sequence2.sv b/regression/verilog/SVA/cover_sequence2.sv index af909572..11731694 100644 --- a/regression/verilog/SVA/cover_sequence2.sv +++ b/regression/verilog/SVA/cover_sequence2.sv @@ -1,15 +1,21 @@ module main(input clk); // count up - reg [7:0] x = 0; + int x = 0; - always @(posedge clk) + always_ff @(posedge clk) x++; // expected to fail p0: cover property (x==2 ##1 x==3 ##1 x==100); - // expected to fail until bound reaches 100 + // expected to fail until x reaches 100 p1: cover property (x==98 ##1 x==99 ##1 x==100); + // expected to pass once x reaches 5 + p2: cover property (x==3 ##1 x==4 ##1 x==5); + + // expected to pass once x reaches 6 + p3: cover property (x==4 ##1 x==5 ##1 x==6); + endmodule diff --git a/regression/verilog/SVA/cover_sequence3.desc b/regression/verilog/SVA/cover_sequence3.desc new file mode 100644 index 00000000..160ef9eb --- /dev/null +++ b/regression/verilog/SVA/cover_sequence3.desc @@ -0,0 +1,11 @@ +CORE +cover_sequence3.sv +--bound 3 +^\[main\.p0\] cover \(1 \[\*10\]\): REFUTED up to bound 3$ +^\[main\.p1\] cover \(1 \[\*4:10\]\): PROVED$ +^\[main\.p2\] cover \(1 \[\*5:10\]\): REFUTED up to bound 3$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/cover_sequence3.sv b/regression/verilog/SVA/cover_sequence3.sv new file mode 100644 index 00000000..09124001 --- /dev/null +++ b/regression/verilog/SVA/cover_sequence3.sv @@ -0,0 +1,18 @@ +module main(input clk); + + // count up + int x = 0; + + always_ff @(posedge clk) + x++; + + // passes with bound >=9 + p0: cover property (1[*10]); + + // passes with bound >=3 + p1: cover property (1[*4:10]); + + // passes with bound >=4 + p2: cover property (1[*5:10]); + +endmodule diff --git a/regression/verilog/SVA/cover_sequence4.desc b/regression/verilog/SVA/cover_sequence4.desc new file mode 100644 index 00000000..22b36589 --- /dev/null +++ b/regression/verilog/SVA/cover_sequence4.desc @@ -0,0 +1,12 @@ +KNOWNBUG +cover_sequence4.sv +--bound 3 +^\[main\.p0\] cover \(1 \[=10\]\): REFUTED up to bound 3$ +^\[main\.p1\] cover \(1 \[=4:10\]\): PROVED$ +^\[main\.p2\] cover \(1 \[=5:10\]\): REFUTED up to bound 3$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Implementation of [=x:y] is missing. diff --git a/regression/verilog/SVA/cover_sequence4.sv b/regression/verilog/SVA/cover_sequence4.sv new file mode 100644 index 00000000..9c08ffb5 --- /dev/null +++ b/regression/verilog/SVA/cover_sequence4.sv @@ -0,0 +1,18 @@ +module main(input clk); + + // count up + int x = 0; + + always_ff @(posedge clk) + x++; + + // passes with bound >=9 + p0: cover property (1[=10]); + + // passes with bound >=3 + p1: cover property (1[=4:10]); + + // passes with bound >=4 + p2: cover property (1[=5:10]); + +endmodule diff --git a/regression/verilog/SVA/strong1.desc b/regression/verilog/SVA/strong1.desc index 6f03056b..2ee4a1bd 100644 --- a/regression/verilog/SVA/strong1.desc +++ b/regression/verilog/SVA/strong1.desc @@ -1,7 +1,7 @@ CORE strong1.sv ---bound 20 -^\[main\.p0\] strong\(##\[0:9\] main\.x == 100\): REFUTED$ +--bound 4 +^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/strong1.sv b/regression/verilog/SVA/strong1.sv index 20231c2b..b6954e32 100644 --- a/regression/verilog/SVA/strong1.sv +++ b/regression/verilog/SVA/strong1.sv @@ -8,7 +8,7 @@ module main; always @(posedge clk) x<=x+1; - // fails - initial p0: assert property (strong(##[0:9] x==100)); + // fails if bound is too low + initial p0: assert property (strong(##[0:9] x==5)); endmodule diff --git a/src/trans-word-level/instantiate_word_level.cpp b/src/trans-word-level/instantiate_word_level.cpp index 6e861589..560125df 100644 --- a/src/trans-word-level/instantiate_word_level.cpp +++ b/src/trans-word-level/instantiate_word_level.cpp @@ -123,40 +123,15 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const expr.id() == ID_typecast && expr.type().id() == ID_bool && to_typecast_expr(expr).op().type().id() == ID_verilog_sva_sequence) { - auto &sequence = to_typecast_expr(expr).op(); - - // sequence expressions -- these may have multiple potential - // match points, and evaluate to true if any of them matches - const auto matches = instantiate_sequence(sequence, t, no_timeframes); - exprt::operandst disjuncts; - disjuncts.reserve(matches.size()); - mp_integer max = t; - - for(auto &match : matches) - { - disjuncts.push_back(match.condition); - max = std::max(max, match.end_time); - } - - return {max, disjunction(disjuncts)}; + // should have been done by property_obligations_rec + PRECONDITION(false); } - else if(expr.id() == ID_sva_sequence_property) + else if( + expr.id() == ID_sva_sequence_property || expr.id() == ID_sva_weak || + expr.id() == ID_sva_strong) { - // sequence expressions -- these may have multiple potential - // match points, and evaluate to true if any of them matches - auto &sequence = to_sva_sequence_property_expr(expr); - const auto matches = instantiate_sequence(sequence, t, no_timeframes); - exprt::operandst disjuncts; - disjuncts.reserve(matches.size()); - mp_integer max = t; - - for(auto &match : matches) - { - disjuncts.push_back(match.condition); - max = std::max(max, match.end_time); - } - - return {max, disjunction(disjuncts)}; + // should have been done by property_obligations_rec + PRECONDITION(false); } else if(expr.id() == ID_verilog_past) { diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 889004a6..6b3a616b 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -530,8 +530,17 @@ static obligationst property_obligations_rec( // The sequence must not match. auto &sequence = to_sva_sequence_property_expr_base(op).sequence(); + // clang-format off + auto semantics = + op.id() == ID_sva_strong ? sva_sequence_semanticst::STRONG + : op.id() == ID_sva_weak ? sva_sequence_semanticst::WEAK + : op.id() == ID_sva_implicit_strong ? sva_sequence_semanticst::STRONG + : op.id() == ID_sva_implicit_weak ? sva_sequence_semanticst::WEAK + : sva_sequence_semanticst::WEAK; + // clang-format on + const auto matches = - instantiate_sequence(sequence, current, no_timeframes); + instantiate_sequence(sequence, semantics, current, no_timeframes); obligationst obligations; @@ -577,10 +586,13 @@ static obligationst property_obligations_rec( auto &implication = to_binary_expr(property_expr); // The LHS is a sequence, the RHS is a property. - // The implication must hold for _all_ matches on the LHS, + // The implication must hold for _all_ (strong) matches on the LHS, // i.e., each pair of LHS match and RHS obligation yields an obligation. - const auto lhs_match_points = - instantiate_sequence(implication.lhs(), current, no_timeframes); + const auto lhs_match_points = instantiate_sequence( + implication.lhs(), + sva_sequence_semanticst::STRONG, + current, + no_timeframes); obligationst result; @@ -620,9 +632,12 @@ static obligationst property_obligations_rec( // the result is a property expression. auto &followed_by = to_sva_followed_by_expr(property_expr); - // get match points for LHS sequence - auto matches = - instantiate_sequence(followed_by.antecedent(), current, no_timeframes); + // get (proper) match points for LHS sequence + auto matches = instantiate_sequence( + followed_by.antecedent(), + sva_sequence_semanticst::STRONG, + current, + no_timeframes); exprt::operandst disjuncts; mp_integer t = current; @@ -663,9 +678,19 @@ static obligationst property_obligations_rec( auto &sequence = to_sva_sequence_property_expr_base(property_expr).sequence(); + // clang-format off + auto semantics = + property_expr.id() == ID_sva_strong ? sva_sequence_semanticst::STRONG + : property_expr.id() == ID_sva_weak ? sva_sequence_semanticst::WEAK + : property_expr.id() == ID_sva_implicit_strong ? sva_sequence_semanticst::STRONG + : property_expr.id() == ID_sva_implicit_weak ? sva_sequence_semanticst::WEAK + : sva_sequence_semanticst::WEAK; + // clang-format on + // sequence expressions -- these may have multiple potential // match points, and evaluate to true if any of them matches - const auto matches = instantiate_sequence(sequence, current, no_timeframes); + const auto matches = + instantiate_sequence(sequence, semantics, current, no_timeframes); exprt::operandst disjuncts; disjuncts.reserve(matches.size()); mp_integer max = current; diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index fead3b91..ffe4d217 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "sequence.h" #include -#include #include #include @@ -20,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com sequence_matchest instantiate_sequence( exprt expr, + sva_sequence_semanticst semantics, const mp_integer &t, const mp_integer &no_timeframes) { @@ -32,17 +32,21 @@ sequence_matchest instantiate_sequence( { const auto u = t + from; - // Do we exceed the bound? Make it 'true' + // Do we exceed the bound? Make it 'false'/'true', depending + // on semantics. if(u >= no_timeframes) { DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return {{no_timeframes - 1, true_exprt()}}; + 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(), u, no_timeframes); + sva_cycle_delay_expr.op(), semantics, u, no_timeframes); } - else + else // ##[from:to] something { mp_integer to; @@ -51,25 +55,34 @@ sequence_matchest instantiate_sequence( DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); to = no_timeframes - 1; } - else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to)) + else if(!sva_cycle_delay_expr.to().is_constant()) throw "failed to convert sva_cycle_delay offsets"; + else + to = numeric_cast_v( + to_constant_expr(sva_cycle_delay_expr.to())); auto lower = t + from; auto upper = t + to; - // Do we exceed the bound? Make it 'true' + // Do we exceed the bound? Make it 'true' if we are doing + // weak semantics. if(upper >= no_timeframes) { - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return {{no_timeframes - 1, true_exprt()}}; + if(semantics == sva_sequence_semanticst::WEAK) + { + DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); + return {{no_timeframes - 1, true_exprt()}}; + } + else + upper = no_timeframes - 1; } sequence_matchest matches; for(mp_integer u = lower; u <= upper; ++u) { - auto sub_result = - instantiate_sequence(sva_cycle_delay_expr.op(), u, no_timeframes); + auto sub_result = instantiate_sequence( + sva_cycle_delay_expr.op(), semantics, u, no_timeframes); for(auto &match : sub_result) matches.push_back(match); } @@ -84,21 +97,25 @@ sequence_matchest instantiate_sequence( // This is the product of the match points on the LHS and RHS const auto lhs_matches = - instantiate_sequence(implication.lhs(), t, no_timeframes); + 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 'true' + // 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"); - return {{no_timeframes - 1, true_exprt()}}; + 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(), t_rhs, no_timeframes); + const auto rhs_matches = instantiate_sequence( + implication.rhs(), semantics, t_rhs, no_timeframes); for(auto &rhs_match : rhs_matches) { @@ -119,9 +136,9 @@ sequence_matchest instantiate_sequence( auto &intersect = to_sva_sequence_intersect_expr(expr); const auto lhs_matches = - instantiate_sequence(intersect.lhs(), t, no_timeframes); + instantiate_sequence(intersect.lhs(), semantics, t, no_timeframes); const auto rhs_matches = - instantiate_sequence(intersect.rhs(), t, no_timeframes); + instantiate_sequence(intersect.rhs(), semantics, t, no_timeframes); sequence_matchest result; @@ -146,7 +163,7 @@ sequence_matchest instantiate_sequence( auto &first_match = to_sva_sequence_first_match_expr(expr); const auto lhs_matches = - instantiate_sequence(first_match.lhs(), t, no_timeframes); + instantiate_sequence(first_match.lhs(), semantics, t, no_timeframes); // the match of seq with the earliest ending clock tick is a // match of first_match (seq) @@ -183,7 +200,7 @@ sequence_matchest instantiate_sequence( auto &throughout = to_sva_sequence_throughout_expr(expr); const auto rhs_matches = - instantiate_sequence(throughout.rhs(), t, no_timeframes); + instantiate_sequence(throughout.rhs(), semantics, t, no_timeframes); sequence_matchest result; @@ -210,7 +227,7 @@ sequence_matchest instantiate_sequence( auto &within_expr = to_sva_sequence_within_expr(expr); const auto matches_rhs = - instantiate_sequence(within_expr.rhs(), t, no_timeframes); + instantiate_sequence(within_expr.rhs(), semantics, t, no_timeframes); sequence_matchest result; @@ -218,8 +235,8 @@ sequence_matchest instantiate_sequence( { for(auto start_lhs = t; start_lhs <= match_rhs.end_time; ++start_lhs) { - auto matches_lhs = - instantiate_sequence(within_expr.lhs(), start_lhs, no_timeframes); + auto matches_lhs = instantiate_sequence( + within_expr.lhs(), semantics, start_lhs, no_timeframes); for(auto &match_lhs : matches_lhs) { @@ -245,8 +262,10 @@ sequence_matchest instantiate_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(expr); - auto matches_lhs = instantiate_sequence(and_expr.lhs(), t, no_timeframes); - auto matches_rhs = instantiate_sequence(and_expr.rhs(), t, no_timeframes); + auto matches_lhs = + instantiate_sequence(and_expr.lhs(), semantics, t, no_timeframes); + auto matches_rhs = + instantiate_sequence(and_expr.rhs(), semantics, t, no_timeframes); sequence_matchest result; @@ -268,7 +287,7 @@ sequence_matchest instantiate_sequence( sequence_matchest result; for(auto &op : expr.operands()) - for(auto &match : instantiate_sequence(op, t, no_timeframes)) + for(auto &match : instantiate_sequence(op, semantics, t, no_timeframes)) result.push_back(match); return result; @@ -277,7 +296,8 @@ sequence_matchest instantiate_sequence( { // x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr); - return instantiate_sequence(repetition.lower(), t, no_timeframes); + return instantiate_sequence( + repetition.lower(), semantics, t, no_timeframes); } else if( expr.id() == ID_sva_sequence_repetition_plus || @@ -355,7 +375,8 @@ sequence_matchest instantiate_sequence( // 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 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()); diff --git a/src/trans-word-level/sequence.h b/src/trans-word-level/sequence.h index 2e8ae3d6..2ea0edc6 100644 --- a/src/trans-word-level/sequence.h +++ b/src/trans-word-level/sequence.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + /// A match for an SVA sequence. class sequence_matcht { @@ -32,6 +34,7 @@ using sequence_matchest = std::vector; /// for the given sequence expression starting at time t [[nodiscard]] sequence_matchest instantiate_sequence( exprt expr, + sva_sequence_semanticst, const mp_integer &t, const mp_integer &no_timeframes);