From e11d6abc103a6fff8557fd04a33e03e70b4a2eaa Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 21 Sep 2024 13:41:08 -0700 Subject: [PATCH] BMC: deduplicate property encoding This removes the duplicated code for encoding temporal operators for word-level BMC from wl_instantiatet. --- src/temporal-logic/normalize_property.cpp | 37 ++- src/temporal-logic/normalize_property.h | 27 ++- src/temporal-logic/temporal_logic.cpp | 7 +- src/trans-word-level/Makefile | 13 +- .../instantiate_word_level.cpp | 217 +---------------- src/trans-word-level/obligations.cpp | 24 ++ src/trans-word-level/obligations.h | 4 + src/trans-word-level/property.cpp | 225 +++++++++++++++++- src/verilog/sva_expr.h | 33 ++- 9 files changed, 340 insertions(+), 247 deletions(-) create mode 100644 src/trans-word-level/obligations.cpp diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index 7f2c6897..40f4947c 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "normalize_property.h" #include +#include #include #include @@ -75,9 +76,8 @@ exprt normalize_pre_implies(implies_exprt expr) exprt normalize_pre_sva_overlapped_implication( sva_overlapped_implication_exprt expr) { - // Same as regular implication if lhs and rhs are not - // sequences. - if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs())) + // Same as regular implication if lhs is not a sequence. + if(!is_SVA_sequence(expr.lhs())) return or_exprt{not_exprt{expr.lhs()}, expr.rhs()}; else return std::move(expr); @@ -86,9 +86,9 @@ exprt normalize_pre_sva_overlapped_implication( exprt normalize_pre_sva_non_overlapped_implication( sva_non_overlapped_implication_exprt expr) { - // Same as a->Xb if lhs and rhs are not sequences. - if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs())) - return or_exprt{not_exprt{expr.lhs()}, X_exprt{expr.rhs()}}; + // Same as a->nexttime b if lhs is not a sequence. + if(!is_SVA_sequence(expr.lhs())) + return or_exprt{not_exprt{expr.lhs()}, sva_nexttime_exprt{expr.rhs()}}; else return std::move(expr); } @@ -125,13 +125,14 @@ exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr) expr.from().is_constant() && numeric_cast_v(to_constant_expr(expr.from())) == 0) { - // ##[0:$] φ --> F φ - return F_exprt{expr.op()}; + // ##[0:$] φ --> s_eventually φ + return sva_s_eventually_exprt{expr.op()}; } else { - // ##[i:$] φ --> ##i F φ - return sva_cycle_delay_exprt{expr.from(), F_exprt{expr.op()}}; + // ##[i:$] φ --> always[i:i] s_eventually φ + return sva_ranged_always_exprt{ + expr.from(), expr.from(), sva_s_eventually_exprt{expr.op()}}; } } else @@ -171,11 +172,13 @@ exprt normalize_property(exprt expr) expr = normalize_pre_sva_or(to_sva_or_expr(expr)); else if(expr.id() == ID_sva_nexttime) { - expr = X_exprt{to_sva_nexttime_expr(expr).op()}; + auto one = natural_typet{}.one_expr(); + expr = sva_ranged_always_exprt{one, one, to_sva_nexttime_expr(expr).op()}; } else if(expr.id() == ID_sva_s_nexttime) { - expr = X_exprt{to_sva_s_nexttime_expr(expr).op()}; + auto one = natural_typet{}.one_expr(); + expr = sva_ranged_always_exprt{one, one, to_sva_s_nexttime_expr(expr).op()}; } else if(expr.id() == ID_sva_indexed_nexttime) { @@ -195,6 +198,16 @@ exprt normalize_property(exprt expr) expr = F_exprt{X_exprt{to_sva_cycle_delay_plus_expr(expr).op()}}; else if(expr.id() == ID_sva_cycle_delay_star) expr = F_exprt{to_sva_cycle_delay_star_expr(expr).op()}; + else if(expr.id() == ID_sva_sequence_concatenation) + { + auto &sequence_concatenation = to_sva_sequence_concatenation_expr(expr); + if(!is_SVA_sequence(sequence_concatenation.lhs())) + { + // a ##0 b --> a && b if a is not a sequence + expr = + and_exprt{sequence_concatenation.lhs(), sequence_concatenation.rhs()}; + } + } else if(expr.id() == ID_sva_if) { auto &sva_if_expr = to_sva_if_expr(expr); diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h index b89df450..905b833b 100644 --- a/src/temporal-logic/normalize_property.h +++ b/src/temporal-logic/normalize_property.h @@ -12,22 +12,34 @@ Author: Daniel Kroening, dkr@amazon.com #include /// This applies the following rewrites: +/// /// cover(φ) --> G¬φ +/// +/// -----Propositional----- /// ¬(a ∨ b) --> ¬a ∧ ¬b /// ¬(a ∧ b) --> ¬a ∨ ¬b /// (a -> b) --> ¬a ∨ b +/// +/// -----SVA----- /// a sva_iff b --> a <-> b /// a sva_implies b --> a -> b /// sva_not a --> ¬a -/// a sva_and b --> a ∧ b if a and b are not SVA sequences -/// a sva_or b --> a ∨ b if a and b are not SVA sequences -/// sva_overlapped_implication --> ¬a ∨ b if a and b are not SVA sequences -/// sva_non_overlapped_implication --> ¬a ∨ Xb if a and b are not SVA sequences +/// a sva_and b --> a ∧ b if a and b are not SVA sequences +/// a sva_or b --> a ∨ b if a and b are not SVA sequences +/// sva_overlapped_implication --> ¬a ∨ b if a is not an SVA sequence +/// sva_non_overlapped_implication --> ¬a ∨ sva_nexttime b if a is not an SVA sequence /// sva_nexttime φ --> Xφ /// sva_nexttime[i] φ --> sva_always[i:i] φ /// sva_s_nexttime φ --> Xφ /// sva_s_nexttime[i] φ --> sva_s_always[i:i] φ /// sva_if --> ? : +/// ##[0:$] φ --> s_eventually φ +/// ##[i:$] φ --> s_nexttime[i] s_eventually φ +/// ##[*] φ --> F φ +/// ##[+] φ --> X F φ +/// strong(φ) --> φ +/// weak(φ) --> φ +/// sva_case --> ? : /// a sva_disable_iff b --> a ∨ b /// a sva_accept_on b --> a ∨ b /// a sva_reject_on b --> ¬a ∧ b @@ -35,15 +47,12 @@ Author: Daniel Kroening, dkr@amazon.com /// a sva_sync_reject_on b --> ¬a ∧ b /// ¬ sva_s_eventually φ --> sva_always ¬φ /// ¬ sva_always φ --> sva_s_eventually ¬φ +/// +/// ----LTL----- /// ¬Xφ --> X¬φ /// ¬¬φ --> φ /// ¬Gφ --> F¬φ /// ¬Fφ --> G¬φ -/// ##[*] φ --> F φ -/// ##[+] φ --> X F φ -/// strong(φ) --> φ -/// weak(φ) --> φ -/// sva_case --> ? : exprt normalize_property(exprt); #endif diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 4344f525..e34065a6 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -85,9 +85,10 @@ bool is_SVA_operator(const exprt &expr) id == ID_sva_sync_accept_on || id == ID_sva_sync_reject_on || id == ID_sva_always || id == ID_sva_ranged_always || id == ID_sva_nexttime || id == ID_sva_s_nexttime || - id == ID_sva_until || id == ID_sva_s_until || - id == ID_sva_until_with || id == ID_sva_s_until_with || - id == ID_sva_eventually || id == ID_sva_s_eventually || + id == ID_sva_indexed_nexttime || id == ID_sva_until || + id == ID_sva_s_until || id == ID_sva_until_with || + id == ID_sva_s_until_with || id == ID_sva_eventually || + id == ID_sva_s_eventually || id == ID_sva_ranged_s_eventually || id == ID_sva_cycle_delay || id == ID_sva_overlapped_followed_by || id == ID_sva_nonoverlapped_followed_by; } diff --git a/src/trans-word-level/Makefile b/src/trans-word-level/Makefile index d432b414..80901963 100644 --- a/src/trans-word-level/Makefile +++ b/src/trans-word-level/Makefile @@ -1,12 +1,13 @@ -SRC = get_trans.cpp \ +SRC = counterexample_word_level.cpp \ + get_trans.cpp \ + obligations.cpp \ + property.cpp \ + trans_trace_word_level.cpp \ + instantiate_word_level.cpp \ show_modules.cpp \ show_module_hierarchy.cpp \ unwind.cpp \ - word_level_trans.cpp \ - property.cpp \ - counterexample_word_level.cpp \ - trans_trace_word_level.cpp \ - instantiate_word_level.cpp + word_level_trans.cpp include ../config.inc include ../common diff --git a/src/trans-word-level/instantiate_word_level.cpp b/src/trans-word-level/instantiate_word_level.cpp index b56bdf8b..287dfe9d 100644 --- a/src/trans-word-level/instantiate_word_level.cpp +++ b/src/trans-word-level/instantiate_word_level.cpp @@ -337,217 +337,6 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const return {max, disjunction(disjuncts)}; } - else if(expr.id()==ID_sva_always) - { - auto &op = to_sva_always_expr(expr).op(); - - exprt::operandst conjuncts; - - for(auto u = t; u < no_timeframes; ++u) - { - conjuncts.push_back(instantiate_rec(op, u).second); - } - - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return {no_timeframes - 1, conjunction(conjuncts)}; - } - else if(expr.id() == ID_sva_ranged_always || expr.id() == ID_sva_s_always) - { - auto &phi = expr.id() == ID_sva_ranged_always - ? to_sva_ranged_always_expr(expr).op() - : to_sva_s_always_expr(expr).op(); - auto &lower = expr.id() == ID_sva_ranged_always - ? to_sva_ranged_always_expr(expr).lower() - : to_sva_s_always_expr(expr).lower(); - auto &upper = expr.id() == ID_sva_ranged_always - ? to_sva_ranged_always_expr(expr).upper() - : to_sva_s_always_expr(expr).upper(); - - auto from_opt = numeric_cast(lower); - if(!from_opt.has_value()) - throw ebmc_errort() << "failed to convert SVA always from index"; - - auto from = t + std::max(mp_integer{0}, *from_opt); - - mp_integer to; - - if(upper.id() == ID_infinity) - { - to = no_timeframes - 1; - } - else - { - auto to_opt = numeric_cast(upper); - if(!to_opt.has_value()) - throw ebmc_errort() << "failed to convert SVA always to index"; - to = std::min(t + *to_opt, no_timeframes - 1); - } - - exprt::operandst conjuncts; - - for(mp_integer c = from; c <= to; ++c) - { - conjuncts.push_back(instantiate_rec(phi, c).second); - } - - return {to, conjunction(conjuncts)}; - } - else if(expr.id() == ID_X) - { - const auto next = t + 1; - - if(next < no_timeframes) - { - return instantiate_rec(to_X_expr(expr).op(), next); - } - else - { - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return {no_timeframes - 1, true_exprt()}; // works on NNF only - } - } - else if(expr.id() == ID_sva_eventually) - { - const auto &eventually_expr = to_sva_eventually_expr(expr); - const auto &op = eventually_expr.op(); - - mp_integer lower; - if(to_integer_non_constant(eventually_expr.lower(), lower)) - throw "failed to convert sva_eventually index"; - - mp_integer upper; - if(to_integer_non_constant(eventually_expr.upper(), upper)) - throw "failed to convert sva_eventually index"; - - // This is weak, and passes if any of the timeframes - // does not exist. - if(t + lower >= no_timeframes || t + upper >= no_timeframes) - { - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return {no_timeframes - 1, true_exprt()}; - } - - exprt::operandst disjuncts = {}; - - for(mp_integer u = t + lower; u <= t + upper; ++u) - disjuncts.push_back(instantiate_rec(op, u).second); - - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return {no_timeframes - 1, disjunction(disjuncts)}; - } - else if( - expr.id() == ID_sva_s_eventually || expr.id() == ID_F || expr.id() == ID_AF) - { - const auto &p = to_unary_expr(expr).op(); - - // The following needs to be satisfied for a counterexample - // to Fp: - // (1) There is a loop from the current state i back to - // some earlier state k < i. - // (1) No state j with k<=k<=i on the lasso satisfies 'p'. - // - // We look backwards instead of forwards so that 't' - // is the last state of the counterexample trace. - // - // Note that this is trivially true when t is zero, - // as a single state cannot demonstrate the loop. - - exprt::operandst conjuncts = {}; - const auto i = t; - - for(mp_integer k = 0; k < i; ++k) - { - exprt::operandst disjuncts = {not_exprt(lasso_symbol(k, i))}; - - for(mp_integer j = k; j <= i; ++j) - { - disjuncts.push_back(instantiate_rec(p, j).second); - } - - conjuncts.push_back(disjunction(disjuncts)); - } - - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return {no_timeframes - 1, conjunction(conjuncts)}; - } - else if(expr.id() == ID_sva_ranged_s_eventually) - { - auto &phi = to_sva_ranged_s_eventually_expr(expr).op(); - auto &lower = to_sva_ranged_s_eventually_expr(expr).lower(); - auto &upper = to_sva_ranged_s_eventually_expr(expr).upper(); - - auto from_opt = numeric_cast(lower); - if(!from_opt.has_value()) - throw ebmc_errort() << "failed to convert SVA s_eventually from index"; - - auto from = t + std::max(mp_integer{0}, *from_opt); - - mp_integer to; - - if(upper.id() == ID_infinity) - { - throw ebmc_errort() - << "failed to convert SVA s_eventually to index (infinity)"; - } - else - { - auto to_opt = numeric_cast(upper); - if(!to_opt.has_value()) - throw ebmc_errort() << "failed to convert SVA s_eventually to index"; - to = std::min(t + *to_opt, no_timeframes - 1); - } - - exprt::operandst disjuncts; - mp_integer time = 0; - - for(mp_integer c = from; c <= to; ++c) - { - auto tmp = instantiate_property(phi, c, no_timeframes, ns); - time = std::max(time, tmp.first); - disjuncts.push_back(tmp.second); - } - - return {time, disjunction(disjuncts)}; - } - else if(expr.id()==ID_sva_until || - expr.id()==ID_sva_s_until) - { - // non-overlapping until - // we need a lasso to refute these - - // we expand: p U q <=> q || (p && X(p U q)) - exprt tmp_q = to_binary_expr(expr).op1(); - tmp_q = instantiate_rec(tmp_q, t).second; - - exprt expansion = to_binary_expr(expr).op0(); - expansion = instantiate_rec(expansion, t).second; - - const auto next = t + 1; - - if(next < no_timeframes) - { - expansion = and_exprt(expansion, instantiate_rec(expr, next).second); - } - - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return {no_timeframes - 1, or_exprt(tmp_q, expansion)}; - } - else if(expr.id()==ID_sva_until_with || - expr.id()==ID_sva_s_until_with) - { - // overlapping until - - // we rewrite using 'next' - binary_exprt tmp = to_binary_expr(expr); - if(expr.id()==ID_sva_until_with) - tmp.id(ID_sva_until); - else - tmp.id(ID_sva_s_until); - - tmp.op1() = X_exprt(tmp.op1()); - - return instantiate_rec(tmp, t); - } else if(expr.id() == ID_verilog_past) { auto &verilog_past = to_verilog_past_expr(expr); @@ -566,6 +355,12 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const return instantiate_rec(verilog_past.what(), t - ticks); } } + else if(is_temporal_operator(expr)) + { + // should have been done by property_obligations_rec + throw ebmc_errort() << "instantiate_word_level got temporal operator " + << expr.id(); + } else { mp_integer max = t; diff --git a/src/trans-word-level/obligations.cpp b/src/trans-word-level/obligations.cpp new file mode 100644 index 00000000..5900abd7 --- /dev/null +++ b/src/trans-word-level/obligations.cpp @@ -0,0 +1,24 @@ +/*******************************************************************\ + +Module: Unwinding the Properties + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "obligations.h" + +#include + +std::pair obligationst::conjunction() const +{ + mp_integer max = 0; + exprt::operandst conjuncts; + for(auto &obligation : map) + { + max = std::max(obligation.first, max); + for(auto &cond : obligation.second) + conjuncts.push_back(cond); + } + return {max, ::conjunction(conjuncts)}; +} diff --git a/src/trans-word-level/obligations.h b/src/trans-word-level/obligations.h index 84eaa69a..a219f230 100644 --- a/src/trans-word-level/obligations.h +++ b/src/trans-word-level/obligations.h @@ -52,6 +52,10 @@ class obligationst for(auto &obligation : obligations.map) add(obligation); } + + /// return the conjunction of all obligations, + /// and the biggest of the timeframes involved + std::pair conjunction() const; }; #endif diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 2316322a..f14805be 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "property.h" #include +#include #include #include #include @@ -169,6 +170,8 @@ bool bmc_supports_SVA_property(const exprt &expr) return true; else if(expr.id() == ID_sva_ranged_always) return true; + else if(expr.id() == ID_sva_s_eventually) + return true; else return false; } @@ -242,6 +245,38 @@ static obligationst property_obligations_rec( return obligations; } + else if(property_expr.id() == ID_sva_eventually) + { + const auto &eventually_expr = to_sva_eventually_expr(property_expr); + const auto &op = eventually_expr.op(); + + mp_integer lower; + if(to_integer_non_constant(eventually_expr.lower(), lower)) + throw "failed to convert sva_eventually index"; + + mp_integer upper; + if(to_integer_non_constant(eventually_expr.upper(), upper)) + throw "failed to convert sva_eventually index"; + + // We rely on NNF. + if(current + lower >= no_timeframes || current + upper >= no_timeframes) + { + DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); + return obligationst{no_timeframes - 1, true_exprt()}; + } + + exprt::operandst disjuncts = {}; + + for(mp_integer u = current + lower; u <= current + upper; ++u) + { + auto obligations_rec = + property_obligations_rec(op, solver, u, no_timeframes, ns); + disjuncts.push_back(obligations_rec.conjunction().second); + } + + DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); + return obligationst{no_timeframes - 1, disjunction(disjuncts)}; + } else if( property_expr.id() == ID_AF || property_expr.id() == ID_F || property_expr.id() == ID_sva_s_eventually) @@ -267,8 +302,9 @@ static obligationst property_obligations_rec( for(mp_integer j = current; j <= k; ++j) { - exprt tmp = instantiate(phi, j, no_timeframes, ns); - disjuncts.push_back(std::move(tmp)); + auto tmp = + property_obligations_rec(phi, solver, j, no_timeframes, ns); + disjuncts.push_back(tmp.conjunction().second); } obligations.add(k, disjunction(disjuncts)); @@ -277,6 +313,49 @@ static obligationst property_obligations_rec( return obligations; } + else if(property_expr.id() == ID_sva_ranged_s_eventually) + { + auto &phi = to_sva_ranged_s_eventually_expr(property_expr).op(); + auto &lower = to_sva_ranged_s_eventually_expr(property_expr).lower(); + auto &upper = to_sva_ranged_s_eventually_expr(property_expr).upper(); + + auto from_opt = numeric_cast(lower); + if(!from_opt.has_value()) + throw ebmc_errort() << "failed to convert SVA s_eventually from index"; + + if(*from_opt < 0) + throw ebmc_errort() << "SVA s_eventually from index must not be negative"; + + auto from = std::min(no_timeframes - 1, current + *from_opt); + + mp_integer to; + + if(upper.id() == ID_infinity) + { + throw ebmc_errort() + << "failed to convert SVA s_eventually to index (infinity)"; + } + else + { + auto to_opt = numeric_cast(upper); + if(!to_opt.has_value()) + throw ebmc_errort() << "failed to convert SVA s_eventually to index"; + to = std::min(current + *to_opt, no_timeframes - 1); + } + + exprt::operandst disjuncts; + mp_integer time = 0; + + for(mp_integer c = from; c <= to; ++c) + { + auto tmp = property_obligations_rec(phi, solver, c, no_timeframes, ns) + .conjunction(); + time = std::max(time, tmp.first); + disjuncts.push_back(tmp.second); + } + + return obligationst{time, disjunction(disjuncts)}; + } else if( property_expr.id() == ID_sva_ranged_always || property_expr.id() == ID_sva_s_always) @@ -295,7 +374,10 @@ static obligationst property_obligations_rec( if(!from_opt.has_value()) throw ebmc_errort() << "failed to convert SVA always from index"; - auto from = std::max(mp_integer{0}, *from_opt); + if(*from_opt < 0) + throw ebmc_errort() << "SVA always from index must not be negative"; + + auto from = current + *from_opt; mp_integer to; @@ -308,7 +390,7 @@ static obligationst property_obligations_rec( auto to_opt = numeric_cast(upper); if(!to_opt.has_value()) throw ebmc_errort() << "failed to convert SVA always to index"; - to = std::min(*to_opt, no_timeframes - 1); + to = std::min(current + *to_opt, no_timeframes - 1); } obligationst obligations; @@ -321,9 +403,85 @@ static obligationst property_obligations_rec( return obligations; } + else if( + property_expr.id() == ID_X || property_expr.id() == ID_sva_nexttime || + property_expr.id() == ID_sva_s_nexttime) + { + const auto next = current + 1; + + auto &phi = [](const exprt &expr) -> const exprt & + { + if(expr.id() == ID_X) + return to_X_expr(expr).op(); + else if(expr.id() == ID_sva_nexttime) + return to_sva_nexttime_expr(expr).op(); + else if(expr.id() == ID_sva_s_nexttime) + return to_sva_s_nexttime_expr(expr).op(); + else + PRECONDITION(false); + }(property_expr); + + if(next < no_timeframes) + { + return property_obligations_rec(phi, solver, next, no_timeframes, ns); + } + else + { + DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); + return obligationst{no_timeframes - 1, true_exprt()}; // works on NNF only + } + } + else if( + property_expr.id() == ID_sva_until || property_expr.id() == ID_sva_s_until) + { + // non-overlapping until + // we need a lasso to refute these + + // we expand: p U q <=> q || (p && X(p U q)) + exprt tmp_q = to_binary_expr(property_expr).op1(); + tmp_q = property_obligations_rec(tmp_q, solver, current, no_timeframes, ns) + .conjunction() + .second; + + exprt expansion = to_binary_expr(property_expr).op0(); + expansion = + property_obligations_rec(expansion, solver, current, no_timeframes, ns) + .conjunction() + .second; + + const auto next = current + 1; + + if(next < no_timeframes) + { + auto obligations_rec = property_obligations_rec( + property_expr, solver, next, no_timeframes, ns); + expansion = and_exprt(expansion, obligations_rec.conjunction().second); + } + + DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); + return obligationst{no_timeframes - 1, or_exprt(tmp_q, expansion)}; + } + else if( + property_expr.id() == ID_sva_until_with || + property_expr.id() == ID_sva_s_until_with) + { + // overlapping until + + // we rewrite using 'next' + binary_exprt tmp = to_binary_expr(property_expr); + if(property_expr.id() == ID_sva_until_with) + tmp.id(ID_sva_until); + else + tmp.id(ID_sva_s_until); + + tmp.op1() = X_exprt{tmp.op1()}; + + return property_obligations_rec(tmp, solver, current, no_timeframes, ns); + } else if(property_expr.id() == ID_and) { - // generate seperate obligations for each conjunct + // Generate seperate sets of obligations for each conjunct, + // and then return the union. obligationst obligations; for(auto &op : to_and_expr(property_expr).operands()) @@ -334,6 +492,63 @@ static obligationst property_obligations_rec( return obligations; } + else if(property_expr.id() == ID_or) + { + // Generate seperate obligations for each disjunct, + // and then 'or' these. + mp_integer t = 0; + exprt::operandst disjuncts; + obligationst obligations; + + for(auto &op : to_or_expr(property_expr).operands()) + { + auto obligations = + property_obligations_rec(op, solver, current, no_timeframes, ns); + auto conjunction = obligations.conjunction(); + t = std::max(t, conjunction.first); + disjuncts.push_back(conjunction.second); + } + + return obligationst{t, disjunction(disjuncts)}; + } + else if(property_expr.id() == ID_implies) + { + // we rely on NNF + auto &implies_expr = to_implies_expr(property_expr); + auto tmp = or_exprt{not_exprt{implies_expr.lhs()}, implies_expr.rhs()}; + return property_obligations_rec(tmp, solver, current, no_timeframes, ns); + } + else if(property_expr.id() == ID_if) + { + // we rely on NNF + auto &if_expr = to_if_expr(property_expr); + auto cond = + instantiate_property(if_expr.cond(), current, no_timeframes, ns).second; + auto obligations_true = + property_obligations_rec( + if_expr.true_case(), solver, current, no_timeframes, ns) + .conjunction(); + auto obligations_false = + property_obligations_rec( + if_expr.false_case(), solver, current, no_timeframes, ns) + .conjunction(); + return obligationst{ + std::max(obligations_true.first, obligations_false.first), + if_exprt{cond, obligations_true.second, obligations_false.second}}; + } + else if( + property_expr.id() == ID_typecast && + to_typecast_expr(property_expr).op().type().id() == ID_bool) + { + // drop reduntant type casts + return property_obligations_rec( + to_typecast_expr(property_expr).op(), solver, current, no_timeframes, ns); + } + else if(property_expr.id() == ID_not) + { + return obligationst{ + instantiate_property(property_expr, current, no_timeframes, ns)}; + } else { return obligationst{ diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 94757d14..c01586f3 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -138,7 +138,10 @@ class sva_indexed_nexttime_exprt : public binary_predicate_exprt { public: sva_indexed_nexttime_exprt(exprt index, exprt op) - : binary_predicate_exprt(std::move(index), ID_sva_nexttime, std::move(op)) + : binary_predicate_exprt( + std::move(index), + ID_sva_indexed_nexttime, + std::move(op)) { } @@ -693,6 +696,34 @@ static inline sva_and_exprt &to_sva_and_expr(exprt &expr) return static_cast(expr); } +class sva_sequence_concatenation_exprt : public binary_predicate_exprt +{ +public: + explicit sva_sequence_concatenation_exprt(exprt op0, exprt op1) + : binary_predicate_exprt( + std::move(op0), + ID_sva_sequence_concatenation, + std::move(op1)) + { + } +}; + +static inline const sva_sequence_concatenation_exprt & +to_sva_sequence_concatenation_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_sequence_concatenation); + sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_sequence_concatenation_exprt & +to_sva_sequence_concatenation_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_sequence_concatenation); + sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + class sva_iff_exprt : public binary_predicate_exprt { public: