From 2c5875041b2988c5a7575ce40ad8224912f18067 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 16 Apr 2025 23:33:42 -0700 Subject: [PATCH 1/2] BMC: remove dead sequence cases Cases relating to sequence expressions are now fully handled in property_obligations_rec. --- .../instantiate_word_level.cpp | 39 ++++--------------- 1 file changed, 7 insertions(+), 32 deletions(-) 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) { From 86b4c586498d9112fdcc1f9daacca5aeaede658e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 18 Apr 2025 12:37:09 -0700 Subject: [PATCH 2/2] BMC: implement weak/strong sequences This implements strong semantics for SVA sequences in the word-level BMC engine. Strong semantics are used with an explicit strong(...) operator or for SVA cover. The difference between weak and strong semantics arises in BMC when the sequence reaches the end of the unwinding: using weak semantics, the sequence matches, whereas using strong semantics the sequence does not. --- regression/verilog/SVA/cover_sequence2.desc | 11 +-- regression/verilog/SVA/cover_sequence2.sv | 12 +++- regression/verilog/SVA/cover_sequence3.desc | 11 +++ regression/verilog/SVA/cover_sequence3.sv | 18 +++++ regression/verilog/SVA/cover_sequence4.desc | 12 ++++ regression/verilog/SVA/cover_sequence4.sv | 18 +++++ regression/verilog/SVA/strong1.desc | 4 +- regression/verilog/SVA/strong1.sv | 4 +- src/trans-word-level/property.cpp | 41 ++++++++--- src/trans-word-level/sequence.cpp | 77 +++++++++++++-------- src/trans-word-level/sequence.h | 3 + 11 files changed, 163 insertions(+), 48 deletions(-) create mode 100644 regression/verilog/SVA/cover_sequence3.desc create mode 100644 regression/verilog/SVA/cover_sequence3.sv create mode 100644 regression/verilog/SVA/cover_sequence4.desc create mode 100644 regression/verilog/SVA/cover_sequence4.sv 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/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);