From 6963c3d6c4fbde66feb84ff10a2eeac308cf4f7b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 23 Apr 2025 13:39:50 -0700 Subject: [PATCH] fix SVA ##[*] and ##[+] Rewriting SVA the sequences ##[*] and ##[+] to SVA eventually properties does not match the weak sequence semantics. This removes the rewrite to a property, and replaces it by a lowering of the operators ##[*] and ##[+] to ##[:]. --- regression/verilog/SVA/sequence2.desc | 14 +++----- regression/verilog/SVA/sequence2.sv | 7 ++-- regression/verilog/SVA/sequence3.desc | 5 ++- regression/verilog/SVA/sequence3.sv | 8 ++--- src/temporal-logic/normalize_property.cpp | 33 ------------------ src/temporal-logic/temporal_logic.cpp | 1 + src/trans-word-level/sequence.cpp | 42 +++++++++++++++-------- src/verilog/sva_expr.cpp | 18 ++++++++++ src/verilog/sva_expr.h | 6 ++++ src/verilog/verilog_typecheck_sva.cpp | 7 ++-- 10 files changed, 71 insertions(+), 70 deletions(-) diff --git a/regression/verilog/SVA/sequence2.desc b/regression/verilog/SVA/sequence2.desc index 57f229c3f..625bf48fd 100644 --- a/regression/verilog/SVA/sequence2.desc +++ b/regression/verilog/SVA/sequence2.desc @@ -1,17 +1,11 @@ -CORE +KNOWNBUG sequence2.sv --bound 10 --numbered-trace -^\[main\.p0] ##\[0:\$\] main\.x == 10: REFUTED$ -^Counterexample with \d+ states:$ -^main\.x@0 = 0$ -^main\.x@1 = 1$ -^main\.x@2 = 2$ -^main\.x@3 = 3$ -^main\.x@4 = 4$ -^main\.x@5 = 5$ -^main\.x@6 = 5$ +^\[main\.p0] ##\[0:\$\] main\.x == 10: PROVED up to bound 10$ +^\[main\.p1] ##\[0:\$\] main\.x == 10: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- +strong(...) is missing. diff --git a/regression/verilog/SVA/sequence2.sv b/regression/verilog/SVA/sequence2.sv index 524445b46..9f2a94402 100644 --- a/regression/verilog/SVA/sequence2.sv +++ b/regression/verilog/SVA/sequence2.sv @@ -9,7 +9,10 @@ module main; if(x != 5) x<=x+1; - // fails once we see the lasso 0, 1, 2, 3, 4, 5, 5 - initial p0: assert property (##[0:$] x==10); + // does not match -- passes + initial p0: assert property (weak(##[0:$] x==10)); + + // does not match -- fails + initial p1: assert property (strong(##[0:$] x==10)); endmodule diff --git a/regression/verilog/SVA/sequence3.desc b/regression/verilog/SVA/sequence3.desc index 4db1f8979..bb6aab765 100644 --- a/regression/verilog/SVA/sequence3.desc +++ b/regression/verilog/SVA/sequence3.desc @@ -1,14 +1,13 @@ -CORE +KNOWNBUG sequence3.sv --bound 20 --numbered-trace ^\[main\.p0\] ##\[\*\] main\.x == 6: REFUTED$ -^Counterexample with 7 states:$ ^\[main\.p1\] ##\[\*\] main\.x == 5: PROVED up to bound 20$ ^\[main\.p2\] ##\[\+\] main\.x == 0: REFUTED$ -^Counterexample with 7 states:$ ^\[main\.p3\] ##\[\+\] main\.x == 5: PROVED up to bound 20$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- +strong(...) is missing diff --git a/regression/verilog/SVA/sequence3.sv b/regression/verilog/SVA/sequence3.sv index bcea5c87f..9e79aa582 100644 --- a/regression/verilog/SVA/sequence3.sv +++ b/regression/verilog/SVA/sequence3.sv @@ -10,11 +10,11 @@ module main; x<=x+1; // ##[*] is the same as [0:$] - initial p0: assert property (##[*] x==6); // should fail - initial p1: assert property (##[*] x==5); // should pass + initial p0: assert property (strong(##[*] x==6)); // no match + initial p1: assert property (strong(##[*] x==5)); // match // ##[+] is the same as [1:$] - initial p2: assert property (##[+] x==0); // should fail - initial p3: assert property (##[+] x==5); // should pass + initial p2: assert property (strong(##[+] x==0)); // no match + initial p3: assert property (strong(##[+] x==5)); // match endmodule diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index f259f4a52..4d9723452 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -34,26 +34,6 @@ exprt normalize_pre_sva_non_overlapped_implication( return std::move(expr); } -exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr) -{ - if(expr.is_unbounded()) - { - if(numeric_cast_v(expr.from()) == 0) - { - // ##[0:$] φ --> s_eventually φ - return sva_s_eventually_exprt{expr.op()}; - } - else - { - // ##[i:$] φ --> always[i:i] s_eventually φ - return sva_ranged_always_exprt{ - expr.from(), expr.from(), sva_s_eventually_exprt{expr.op()}}; - } - } - else - return std::move(expr); -} - exprt normalize_property_rec(exprt expr) { // pre-traversal @@ -84,19 +64,6 @@ exprt normalize_property_rec(exprt expr) expr = sva_s_always_exprt{ nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()}; } - else if(expr.id() == ID_sva_cycle_delay) - { - expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr)); - } - else if(expr.id() == ID_sva_cycle_delay_plus) - { - expr = sva_s_nexttime_exprt{ - sva_s_eventually_exprt{to_sva_cycle_delay_plus_expr(expr).op()}}; - } - else if(expr.id() == ID_sva_cycle_delay_star) - { - expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()}; - } // normalize the operands for(auto &op : expr.operands()) diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index d92c49549..832447485 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -106,6 +106,7 @@ bool is_SVA_sequence_operator(const exprt &expr) // are property expressions, not sequence expressions. // 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 || diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index fead3b91f..1806778ff 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -42,30 +42,35 @@ sequence_matchest instantiate_sequence( return instantiate_sequence( sva_cycle_delay_expr.op(), u, no_timeframes); } - else + else // a range { - mp_integer to; + auto lower = t + from; + mp_integer upper; if(sva_cycle_delay_expr.to().id() == ID_infinity) { DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - to = no_timeframes - 1; + upper = no_timeframes; + } + else + { + mp_integer to; + if(to_integer_non_constant(sva_cycle_delay_expr.to(), to)) + throw "failed to convert sva_cycle_delay offsets"; + upper = t + to; } - else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to)) - throw "failed to convert sva_cycle_delay offsets"; - auto lower = t + from; - auto upper = t + to; + sequence_matchest matches; - // Do we exceed the bound? Make it 'true' + // Do we exceed the bound? Add an unconditional match. if(upper >= no_timeframes) { DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return {{no_timeframes - 1, true_exprt()}}; + matches.emplace_back(no_timeframes - 1, true_exprt()); + upper = no_timeframes - 1; } - sequence_matchest matches; - + // Add a potential match for each timeframe in the range for(mp_integer u = lower; u <= upper; ++u) { auto sub_result = @@ -77,6 +82,16 @@ sequence_matchest instantiate_sequence( return matches; } } + else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something + { + auto &cycle_delay_star = to_sva_cycle_delay_star_expr(expr); + return instantiate_sequence(cycle_delay_star.lower(), 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(cycle_delay_plus.lower(), t, no_timeframes); + } else if(expr.id() == ID_sva_sequence_concatenation) { auto &implication = to_binary_expr(expr); @@ -378,8 +393,7 @@ sequence_matchest instantiate_sequence( else { // not a sequence, evaluate as state predicate - auto obligations = property_obligations(expr, t, no_timeframes); - auto conjunction = obligations.conjunction(); - return {{conjunction.first, conjunction.second}}; + auto instantiated = instantiate_property(expr, t, no_timeframes); + return {{instantiated.first, instantiated.second}}; } } diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp index 476bf1e4b..81a1bac13 100644 --- a/src/verilog/sva_expr.cpp +++ b/src/verilog/sva_expr.cpp @@ -11,6 +11,24 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +exprt sva_cycle_delay_plus_exprt::lower() const +{ + // same as ##[1:$] + return sva_cycle_delay_exprt{ + from_integer(1, integer_typet{}), + exprt{ID_infinity, integer_typet{}}, + op()}; +} + +exprt sva_cycle_delay_star_exprt::lower() const +{ + // same as ##[0:$] + return sva_cycle_delay_exprt{ + from_integer(0, integer_typet{}), + exprt{ID_infinity, integer_typet{}}, + op()}; +} + exprt sva_case_exprt::lowering() const { auto &case_items = this->case_items(); diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 219789518..e6781af55 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -1004,6 +1004,9 @@ class sva_cycle_delay_plus_exprt : public unary_exprt : unary_exprt(ID_sva_cycle_delay_plus, std::move(op), bool_typet()) { } + + // ##[1:$] op + exprt lower() const; }; static inline const sva_cycle_delay_plus_exprt & @@ -1029,6 +1032,9 @@ class sva_cycle_delay_star_exprt : public unary_exprt : unary_exprt(ID_sva_cycle_delay_star, std::move(op), bool_typet()) { } + + // ##[0:$] op + exprt lower() const; }; static inline const sva_cycle_delay_star_exprt & diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index b85fb3e23..cf6f0785c 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -77,8 +77,7 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr) { if( expr.id() == ID_sva_not || expr.id() == ID_sva_always || - expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay_plus || - expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_nexttime || + expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime) { convert_sva(expr.op()); @@ -87,8 +86,8 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr) return std::move(expr); } else if( - expr.id() == ID_sva_cycle_delay_plus || - expr.id() == ID_sva_cycle_delay_star || + expr.id() == ID_sva_cycle_delay_plus || // ##[+] + expr.id() == ID_sva_cycle_delay_star || // ##[*] expr.id() == ID_sva_sequence_repetition_plus || // x[+] expr.id() == ID_sva_sequence_repetition_star) // x[*} {