From a17f7a1ada4e6177aeeb11640fb96580b6957954 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 1 Nov 2025 18:10:19 -0700 Subject: [PATCH] SVA->Buechi: enable fragment of strong sequences The SVA to Buechi conversion can support strong sequences that have finite counterexamples. This enables these cases. --- .../sva-buechi/cover_sequence1.bmc.desc | 4 +- .../sva-buechi/cover_sequence2.bmc.desc | 8 +- .../ebmc-spot/sva-buechi/sequence2.bmc.desc | 2 +- .../ebmc-spot/sva-buechi/sequence3.bmc.desc | 8 +- regression/ebmc-spot/sva-buechi/strong1.desc | 2 +- .../sva-buechi/system_verilog_assertion4.desc | 4 +- src/temporal-logic/ltl_sva_to_string.cpp | 75 +++++++++++++++---- src/temporal-logic/ltl_sva_to_string.h | 7 +- 8 files changed, 80 insertions(+), 30 deletions(-) diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc index 128b3c8a0..a733cbc4d 100644 --- a/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc @@ -1,8 +1,8 @@ CORE ../../verilog/SVA/cover_sequence1.sv --buechi --bound 10 --numbered-trace -^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ -^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ +^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): PROVED$ +^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): REFUTED up to bound 10$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc index cfdbfd026..52b942489 100644 --- a/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc @@ -1,10 +1,10 @@ CORE ../../verilog/SVA/cover_sequence2.sv --buechi --bound 5 -^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ -^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ -^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ -^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ +^\[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$ -- diff --git a/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc index 72b846c4d..5f44b56c6 100644 --- a/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc @@ -2,7 +2,7 @@ CORE ../../verilog/SVA/sequence2.sv --buechi --bound 10 ^\[main\.p0] weak\(##\[0:\$\] main\.x == 10\): PROVED up to bound 10$ -^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: sva_strong not convertible to Buechi$ +^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: sva_cycle_delay not convertible to Buechi$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc index c8f1429e8..e09e8a230 100644 --- a/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc @@ -1,10 +1,10 @@ CORE ../../verilog/SVA/sequence3.sv --buechi --bound 20 --numbered-trace -^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): UNSUPPORTED: sva_strong not convertible to Buechi$ -^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$ -^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): UNSUPPORTED: sva_strong not convertible to Buechi$ -^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$ +^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): UNSUPPORTED: sva_cycle_delay_star not convertible to Buechi$ +^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): UNSUPPORTED: sva_cycle_delay_star not convertible to Buechi$ +^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): UNSUPPORTED: sva_cycle_delay_plus not convertible to Buechi$ +^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): UNSUPPORTED: sva_cycle_delay_plus not convertible to Buechi$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/strong1.desc b/regression/ebmc-spot/sva-buechi/strong1.desc index c65dd91b6..4836a4e3b 100644 --- a/regression/ebmc-spot/sva-buechi/strong1.desc +++ b/regression/ebmc-spot/sva-buechi/strong1.desc @@ -1,7 +1,7 @@ CORE ../../verilog/SVA/strong1.sv --buechi --bound 4 -^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$ +^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: sva_cycle_delay not convertible to Buechi$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc b/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc index 5318a533f..8b1fab46a 100644 --- a/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc +++ b/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc @@ -1,8 +1,8 @@ CORE ../../verilog/SVA/system_verilog_assertion4.sv --buechi --module main --bound 10 -^\[main\.p11\] always \(main\.x == 0 \|-> \(\(##1 main\.x == 1\) and \(not \(##2 main\.x == 3\)\)\)\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$ -^EXIT=10$ +^\[main\.p11\] always \(main\.x == 0 \|-> \(\(##1 main\.x == 1\) and \(not \(##2 main\.x == 3\)\)\)\): PROVED up to bound 10$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp index 294295b4c..32dd9f048 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -305,42 +305,54 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) { PRECONDITION(mode == PROPERTY); auto &sequence = to_sva_sequence_property_expr_base(expr).sequence(); - auto op_rec = rec(sequence, SVA_SEQUENCE); + auto op_rec = rec(sequence, SVA_SEQUENCE_WEAK); // weak closure return resultt{precedencet::ATOM, '{' + op_rec.s + '}'}; } else if(expr.id() == ID_sva_strong || expr.id() == ID_sva_implicit_strong) { - throw ltl_sva_to_string_unsupportedt{expr}; + PRECONDITION(mode == PROPERTY); + auto &sequence = to_sva_sequence_property_expr_base(expr).sequence(); + auto op_rec = rec(sequence, SVA_SEQUENCE_STRONG); + + // we use the weak closure, and reject cases where this does not work + return resultt{precedencet::ATOM, '{' + op_rec.s + '}'}; } else if(expr.id() == ID_sva_or) { // can be sequence or property - PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE); + PRECONDITION( + mode == PROPERTY || mode == SVA_SEQUENCE_STRONG || + mode == SVA_SEQUENCE_WEAK); return infix("|", expr, mode); } else if(expr.id() == ID_sva_and) { // can be sequence or property - PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE); + PRECONDITION( + mode == PROPERTY || mode == SVA_SEQUENCE_STRONG || + mode == SVA_SEQUENCE_WEAK); // NLM intersection return infix("&", expr, mode); } else if(expr.id() == ID_sva_sequence_intersect) { - PRECONDITION(mode == SVA_SEQUENCE); + PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK); return infix("&&", expr, mode); } else if(expr.id() == ID_sva_boolean) { // can be sequence or property - PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE); + PRECONDITION( + mode == PROPERTY || mode == SVA_SEQUENCE_STRONG || + mode == SVA_SEQUENCE_WEAK); return rec(to_sva_boolean_expr(expr).op(), BOOLEAN); } else if(expr.id() == ID_sva_cycle_delay) { - PRECONDITION(mode == SVA_SEQUENCE); + PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK); + auto &delay = to_sva_cycle_delay_expr(expr); if(delay.lhs().is_nil()) @@ -349,6 +361,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) if(delay.is_range()) // ##[from:to] rhs { + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + auto from = numeric_cast_v(delay.from()); if(delay.is_unbounded()) // ##[n:$] rhs @@ -384,6 +399,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) if(delay.is_range()) { + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + auto from = numeric_cast_v(delay.from()); if(from == 0) @@ -393,6 +411,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } else if(delay.is_unbounded()) // f ##[n:$] g { + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + return infix( " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode); } @@ -427,7 +448,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) { // ##[*] x ---> 1[*] ; x // w ##[*] x ---> w : 1[*] ; x - PRECONDITION(mode == SVA_SEQUENCE); + PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK); + + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + auto &cycle_delay_expr = to_sva_cycle_delay_star_expr(expr); if(cycle_delay_expr.has_lhs()) { @@ -448,7 +473,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) { // ##[+] x ---> 1[+] ; x // w ##[+] x ---> w : 1[+] ; x - PRECONDITION(mode == SVA_SEQUENCE); + PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK); + + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + auto &cycle_delay_expr = to_sva_cycle_delay_plus_expr(expr); if(cycle_delay_expr.has_lhs()) { @@ -477,11 +506,14 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) expr.id() == ID_sva_sequence_repetition_star) // [*] or [*n] or [*x:y] or [*x:$] { - PRECONDITION(mode == SVA_SEQUENCE); + PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK); auto &repetition = to_sva_sequence_repetition_star_expr(expr); unary_exprt new_expr{ID_sva_sequence_repetition_star, repetition.op()}; if(!repetition.repetitions_given()) { + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + return suffix("[*]", new_expr, mode); } else if(repetition.is_empty_match()) @@ -504,6 +536,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } else if(repetition.is_unbounded()) { + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + auto from = numeric_cast_v(repetition.from()); return suffix("[*" + integer2string(from) + "..]", new_expr, mode); } @@ -512,7 +547,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } else if(expr.id() == ID_sva_sequence_repetition_plus) // something[+] { - PRECONDITION(mode == SVA_SEQUENCE); + PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK); + + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + auto new_expr = unary_exprt{ ID_sva_sequence_repetition_plus, to_sva_sequence_repetition_plus_expr(expr).op()}; @@ -523,7 +562,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) // ltl2tgba produces the wrong anser for [->n] and [=n] throw ltl_sva_to_string_unsupportedt{expr}; - PRECONDITION(mode == SVA_SEQUENCE); + PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK); auto &repetition = to_sva_sequence_goto_repetition_expr(expr); unary_exprt new_expr{ID_sva_sequence_goto_repetition, repetition.op()}; if(repetition.is_singleton()) @@ -542,6 +581,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } else if(repetition.is_unbounded()) { + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + auto from = numeric_cast_v(repetition.from()); return suffix("[->" + integer2string(from) + "..]", new_expr, mode); } @@ -554,7 +596,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) // ltl2tgba produces the wrong anser for [->n] and [=n] throw ltl_sva_to_string_unsupportedt{expr}; - PRECONDITION(mode == SVA_SEQUENCE); + PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK); auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr); unary_exprt new_expr{ ID_sva_sequence_non_consecutive_repetition, repetition.op()}; @@ -574,6 +616,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } else if(repetition.is_unbounded()) { + if(mode == SVA_SEQUENCE_STRONG) + throw ltl_sva_to_string_unsupportedt{expr}; + auto from = numeric_cast_v(repetition.from()); return suffix("[=" + integer2string(from) + "..]", new_expr, mode); } @@ -583,9 +628,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } else if(expr.id() == ID_sva_sequence_first_match) // first_match(...) { - PRECONDITION(mode == SVA_SEQUENCE); + PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK); auto &sequence = to_sva_sequence_first_match_expr(expr).sequence(); - auto op_rec = rec(sequence, SVA_SEQUENCE); + auto op_rec = rec(sequence, mode); return resultt{precedencet::ATOM, "first_match(" + op_rec.s + ')'}; } else if(!is_temporal_operator(expr)) diff --git a/src/temporal-logic/ltl_sva_to_string.h b/src/temporal-logic/ltl_sva_to_string.h index f4ac209da..e1bdea976 100644 --- a/src/temporal-logic/ltl_sva_to_string.h +++ b/src/temporal-logic/ltl_sva_to_string.h @@ -57,7 +57,12 @@ class ltl_sva_to_stringt // Spot may or may not use the same numbering in the AP header. numberingt atoms; - using modet = enum { PROPERTY, SVA_SEQUENCE, BOOLEAN }; + using modet = enum { + PROPERTY, + SVA_SEQUENCE_STRONG, + SVA_SEQUENCE_WEAK, + BOOLEAN + }; resultt prefix(std::string s, const unary_exprt &, modet); resultt suffix(std::string s, const unary_exprt &, modet);