diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp index c90b73b4c..219533bdc 100644 --- a/src/ebmc/k_induction.cpp +++ b/src/ebmc/k_induction.cpp @@ -11,7 +11,8 @@ Author: Daniel Kroening, daniel.kroening@inf.ethz.ch #include #include -#include +#include +#include #include #include @@ -261,7 +262,8 @@ void k_inductiont::induction_step() const exprt &p = to_unary_expr(property.normalized_expr).op(); for(std::size_t c = 0; c < no_timeframes; c++) { - exprt tmp = instantiate(p, c, no_timeframes); + exprt tmp = + property_obligations(p, c, no_timeframes).conjunction().second; solver.set_to_true(tmp); } } @@ -272,13 +274,16 @@ void k_inductiont::induction_step() // assumption: time frames 0,...,k-1 for(std::size_t c = 0; c < no_timeframes - 1; c++) { - exprt tmp = instantiate(p, c, no_timeframes - 1); + exprt tmp = + property_obligations(p, c, no_timeframes - 1).conjunction().second; solver.set_to_true(tmp); } // property: time frame k { - exprt tmp = instantiate(p, no_timeframes - 1, no_timeframes); + exprt tmp = property_obligations(p, no_timeframes - 1, no_timeframes) + .conjunction() + .second; solver.set_to_false(tmp); } diff --git a/src/temporal-logic/nnf.cpp b/src/temporal-logic/nnf.cpp index 87efbd1b6..dbe321f40 100644 --- a/src/temporal-logic/nnf.cpp +++ b/src/temporal-logic/nnf.cpp @@ -136,6 +136,10 @@ std::optional negate_property_node(const exprt &expr) auto not_b = not_exprt{followed_by.property()}; return sva_non_overlapped_implication_exprt{followed_by.lhs(), not_b}; } + else if(expr.id() == ID_sva_not) + { + return to_sva_not_expr(expr).op(); + } else return {}; } diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index 237c91b22..685020fda 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -182,7 +182,7 @@ exprt normalize_property(exprt expr) expr = trivial_sva(expr); // now do recursion - expr = normalize_property_rec(expr); + // expr = normalize_property_rec(expr); return expr; } diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index b3c7e50fa..c0da90fb8 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -72,6 +72,7 @@ bool is_SVA_sequence(const exprt &expr) return id == ID_sva_and || id == ID_sva_or || id == ID_sva_overlapped_implication || id == ID_sva_non_overlapped_implication || 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 || @@ -79,7 +80,8 @@ bool is_SVA_sequence(const exprt &expr) id == ID_sva_sequence_consecutive_repetition || id == ID_sva_sequence_non_consecutive_repetition || id == ID_sva_sequence_repetition_star || - id == ID_sva_sequence_repetition_plus; + id == ID_sva_sequence_repetition_plus || id == ID_sva_strong || + id == ID_sva_weak; } bool is_SVA_operator(const exprt &expr) diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 60d6d87e9..d4e663484 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -399,6 +399,20 @@ static obligationst property_obligations_rec( return obligationst{no_timeframes - 1, true_exprt()}; // works on NNF only } } + else if(property_expr.id() == ID_sva_indexed_nexttime) + { + auto &nexttime = to_sva_indexed_nexttime_expr(property_expr); + auto always = sva_ranged_always_exprt{ + nexttime.index(), nexttime.index(), nexttime.op()}; + return property_obligations_rec(always, current, no_timeframes); + } + else if(property_expr.id() == ID_sva_indexed_s_nexttime) + { + auto &nexttime = to_sva_indexed_s_nexttime_expr(property_expr); + auto s_always = sva_ranged_always_exprt{ + nexttime.index(), nexttime.index(), nexttime.op()}; + return property_obligations_rec(s_always, current, no_timeframes); + } else if(property_expr.id() == ID_sva_s_until || property_expr.id() == ID_U) { auto &p = to_binary_expr(property_expr).lhs(); diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index 3f4f0e73c..20dd30026 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -176,6 +176,26 @@ std::vector> instantiate_sequence( return result; } + else if(expr.id() == ID_sva_strong || expr.id() == ID_sva_weak) + { + // not distinguished + auto &op = to_unary_expr(expr).op(); + return instantiate_sequence(op, t, no_timeframes); + } + else if(expr.id() == ID_sva_cycle_delay_plus) + { + auto new_expr = sva_s_eventually_exprt{ + sva_s_nexttime_exprt{to_sva_cycle_delay_plus_expr(expr).op()}}; + auto obligations = property_obligations(new_expr, t, no_timeframes); + return {obligations.conjunction()}; + } + else if(expr.id() == ID_sva_cycle_delay_star) + { + auto new_expr = + sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()}; + auto obligations = property_obligations(new_expr, t, no_timeframes); + return {obligations.conjunction()}; + } else { // not a sequence, evaluate as state predicate diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index f0b065459..f34c589dd 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -657,6 +657,11 @@ class sva_not_exprt : public unary_predicate_exprt : unary_predicate_exprt(ID_sva_not, std::move(op)) { } + + not_exprt lower() const + { + return not_exprt{op()}; + } }; static inline const sva_not_exprt &to_sva_not_expr(const exprt &expr) @@ -731,6 +736,11 @@ class sva_iff_exprt : public binary_predicate_exprt : binary_predicate_exprt(std::move(op0), ID_sva_iff, std::move(op1)) { } + + equal_exprt lower() const + { + return equal_exprt{lhs(), rhs()}; + } }; static inline const sva_iff_exprt &to_sva_iff_expr(const exprt &expr) @@ -754,6 +764,11 @@ class sva_implies_exprt : public binary_predicate_exprt : binary_predicate_exprt(std::move(op0), ID_sva_implies, std::move(op1)) { } + + implies_exprt lower() const + { + return implies_exprt{lhs(), rhs()}; + } }; static inline const sva_implies_exprt &to_sva_implies_expr(const exprt &expr)