From 339ecda3ca50fb80566bc109e48a1b1410d92a0c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 30 May 2025 09:28:44 -0700 Subject: [PATCH] SVA-to-Buechi: sequence repetition operators This adds conversion for [*...], [=...], [->...], [+] to the SVA-to-Buechi translation. --- .../sva-buechi/sequence_repetition4.desc | 10 ++ .../sva-buechi/sequence_repetition5.desc | 10 ++ .../sva-buechi/sequence_repetition6.desc | 8 -- .../sva-buechi/sequence_repetition7.desc | 10 ++ src/temporal-logic/ltl_sva_to_string.cpp | 99 +++++++++++++++++++ src/verilog/sva_expr.h | 20 +++- 6 files changed, 144 insertions(+), 13 deletions(-) create mode 100644 regression/ebmc-spot/sva-buechi/sequence_repetition4.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_repetition5.desc delete mode 100644 regression/ebmc-spot/sva-buechi/sequence_repetition6.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_repetition7.desc diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition4.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition4.desc new file mode 100644 index 00000000..b558d23a --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition4.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/sequence_repetition4.sv +--buechi --bound 10 +^\[main\.p0\] \(main\.x == 0 ##1 main\.x == 1\) \[\*2\]: PROVED up to bound \d+$ +^\[main\.p1\] \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 0\) \[\*2\]: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc new file mode 100644 index 00000000..b7d763a4 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/sequence_repetition5.sv +--buechi --bound 20 +^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$ +^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition6.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition6.desc deleted file mode 100644 index c33fee5a..00000000 --- a/regression/ebmc-spot/sva-buechi/sequence_repetition6.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -../../verilog/SVA/sequence_repetition6.sv ---buechi -^file .* line 4: sequence required, but got property$ -^EXIT=2$ -^SIGNAL=0$ --- --- diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition7.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition7.desc new file mode 100644 index 00000000..f271821d --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition7.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/sequence_repetition7.sv +--buechi --bound 20 +^\[.*\] \(main\.a ##1 main\.b\) \[\*5\]: PROVED up to bound 20$ +^\[.*\] \(\!main\.b ##1 \!main\.a\) \[\*5\]: PROVED up to bound 20$ +^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 5e451d33..7523956b 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -433,6 +433,105 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) auto a2 = and_exprt{not_exprt{if_expr.cond()}, if_expr.false_case()}; return rec(or_exprt{a1, a2}, mode); } + else if( + expr.id() == + ID_sva_sequence_repetition_star) // [*] or [*n] or [*x:y] or [*x:$] + { + PRECONDITION(mode == SVA_SEQUENCE); + auto &repetition = to_sva_sequence_repetition_star_expr(expr); + unary_exprt new_expr{ID_sva_sequence_repetition_star, repetition.op()}; + if(!repetition.repetitions_given()) + { + return suffix("[*]", new_expr, mode); + } + else if(repetition.is_empty_match()) + { + throw ebmc_errort{} << "cannot convert [*0] to Buechi"; + } + else if(repetition.is_singleton()) + { + auto n = numeric_cast_v(repetition.repetitions()); + return suffix("[*" + integer2string(n) + "]", new_expr, mode); + } + else if(repetition.is_bounded_range()) + { + auto from = numeric_cast_v(repetition.from()); + auto to = numeric_cast_v(repetition.to()); + return suffix( + "[*" + integer2string(from) + ".." + integer2string(to) + "]", + new_expr, + mode); + } + else if(repetition.is_unbounded()) + { + auto from = numeric_cast_v(repetition.from()); + return suffix("[*" + integer2string(from) + "..]", new_expr, mode); + } + else + DATA_INVARIANT(false, "unexpected sva_sequence_repetition_star"); + } + else if(expr.id() == ID_sva_sequence_repetition_plus) // something[+] + { + PRECONDITION(mode == SVA_SEQUENCE); + return suffix("[+]", expr, mode); + } + else if(expr.id() == ID_sva_sequence_goto_repetition) // something[->n] + { + PRECONDITION(mode == SVA_SEQUENCE); + auto &repetition = to_sva_sequence_goto_repetition_expr(expr); + unary_exprt new_expr{ID_sva_sequence_goto_repetition, repetition.op()}; + if(repetition.is_singleton()) + { + auto n = numeric_cast_v(repetition.repetitions()); + return suffix("[->" + integer2string(n) + "]", new_expr, mode); + } + else if(repetition.is_bounded_range()) + { + auto from = numeric_cast_v(repetition.from()); + auto to = numeric_cast_v(repetition.to()); + return suffix( + "[->" + integer2string(from) + ".." + integer2string(to) + "]", + new_expr, + mode); + } + else if(repetition.is_unbounded()) + { + auto from = numeric_cast_v(repetition.from()); + return suffix("[->" + integer2string(from) + "..]", new_expr, mode); + } + else + DATA_INVARIANT(false, "unexpected sva_sequence_goto_repetition"); + } + else if( + expr.id() == ID_sva_sequence_non_consecutive_repetition) // something[=n] + { + PRECONDITION(mode == SVA_SEQUENCE); + auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr); + unary_exprt new_expr{ + ID_sva_sequence_non_consecutive_repetition, repetition.op()}; + if(repetition.is_singleton()) + { + auto n = numeric_cast_v(repetition.repetitions()); + return suffix("[=" + integer2string(n) + "]", new_expr, mode); + } + else if(repetition.is_bounded_range()) + { + auto from = numeric_cast_v(repetition.from()); + auto to = numeric_cast_v(repetition.to()); + return suffix( + "[=" + integer2string(from) + ".." + integer2string(to) + "]", + new_expr, + mode); + } + else if(repetition.is_unbounded()) + { + auto from = numeric_cast_v(repetition.from()); + return suffix("[=" + integer2string(from) + "..]", new_expr, mode); + } + else + DATA_INVARIANT( + false, "unexpected sva_sequence_non_consecutive_repetition"); + } else if(!is_temporal_operator(expr)) { auto number = atoms.number(expr); diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 2f410f8d..43600534 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -1456,19 +1456,19 @@ class sva_sequence_repetition_exprt : public ternary_exprt /// op[*0] is a special case, denoting the empty match bool is_empty_match() const { - return !is_range() && repetitions_given() && op1().is_zero(); + return is_singleton() && op1().is_zero(); } // The number of repetitions must be a constant after elaboration. const constant_exprt &repetitions() const { - PRECONDITION(repetitions_given() && !is_range()); + PRECONDITION(is_singleton()); return static_cast(op1()); } constant_exprt &repetitions() { - PRECONDITION(repetitions_given() && !is_range()); + PRECONDITION(is_singleton()); return static_cast(op1()); } @@ -1477,6 +1477,16 @@ class sva_sequence_repetition_exprt : public ternary_exprt return op2().is_not_nil(); } + bool is_bounded_range() const + { + return op2().is_not_nil() && op2().id() != ID_infinity; + } + + bool is_singleton() const + { + return op1().is_not_nil() && op2().is_nil(); + } + bool is_unbounded() const { return op2().id() == ID_infinity; @@ -1496,13 +1506,13 @@ class sva_sequence_repetition_exprt : public ternary_exprt const constant_exprt &to() const { - PRECONDITION(is_range() && !is_unbounded()); + PRECONDITION(is_bounded_range()); return static_cast(op2()); } constant_exprt &to() { - PRECONDITION(is_range() && !is_unbounded()); + PRECONDITION(is_bounded_range()); return static_cast(op2()); }