From 1f8f975725236a1e18772a457f8faf1bd8c1e728 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 30 Sep 2024 13:51:50 -0700 Subject: [PATCH] word-level BMC: allow SVA and/or/implies at property level --- regression/verilog/SVA/sva_iff2.desc | 8 ++++++ regression/verilog/SVA/sva_iff2.sv | 11 ++++++++ src/temporal-logic/nnf.cpp | 17 +++++++++++ src/trans-word-level/property.cpp | 42 ++++++++++++++++++++++++++++ src/trans-word-level/property.h | 7 +++++ src/trans-word-level/sequence.cpp | 15 ++++++---- 6 files changed, 94 insertions(+), 6 deletions(-) create mode 100644 regression/verilog/SVA/sva_iff2.desc create mode 100644 regression/verilog/SVA/sva_iff2.sv diff --git a/regression/verilog/SVA/sva_iff2.desc b/regression/verilog/SVA/sva_iff2.desc new file mode 100644 index 000000000..d57581691 --- /dev/null +++ b/regression/verilog/SVA/sva_iff2.desc @@ -0,0 +1,8 @@ +CORE +sva_iff2.sv +--bound 10 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/sva_iff2.sv b/regression/verilog/SVA/sva_iff2.sv new file mode 100644 index 000000000..f10bfc315 --- /dev/null +++ b/regression/verilog/SVA/sva_iff2.sv @@ -0,0 +1,11 @@ +module main(input a, b); + + // p0: assert property ((always a) iff (always a)); + p1: assert property ((eventually[0:1] a) iff (eventually[0:1] a)); + // p2: assert property ((s_eventually a) iff (s_eventually a)); + p3: assert property ((a until b) iff (a until b)); + // p4: assert property ((a s_until b) iff (a s_until a)); + p5: assert property ((a until_with b) iff (a until_with b)); + p6: assert property ((a s_until_with b) iff (a s_until_with a)); + +endmodule diff --git a/src/temporal-logic/nnf.cpp b/src/temporal-logic/nnf.cpp index 429597d6d..85cddad5e 100644 --- a/src/temporal-logic/nnf.cpp +++ b/src/temporal-logic/nnf.cpp @@ -68,6 +68,23 @@ std::optional negate_property_node(const exprt &expr) { return to_not_expr(expr).op(); } + else if(expr.id() == ID_sva_always) + { + // not always p --> s_eventually not p + return sva_s_eventually_exprt{not_exprt{to_sva_always_expr(expr).op()}}; + } + else if(expr.id() == ID_sva_s_eventually) + { + // not s_eventually p --> always not p + return sva_always_exprt{not_exprt{to_sva_s_eventually_expr(expr).op()}}; + } + else if(expr.id() == ID_sva_eventually) + { + // not eventually[i:j] p --> s_always[i:j] not p + auto &eventually = to_sva_eventually_expr(expr); + return sva_s_always_exprt{ + eventually.lower(), eventually.upper(), not_exprt{eventually.op()}}; + } else if(expr.id() == ID_sva_until) { // ¬(φ W ψ) ≡ (¬φ strongR ¬ψ) diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index bd94e51d9..cea496567 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -519,6 +519,11 @@ static obligationst property_obligations_rec( return property_obligations_rec( op_negated_opt.value(), current, no_timeframes); } + else if(is_SVA_sequence(op)) + { + return obligationst{ + instantiate_property(property_expr, current, no_timeframes)}; + } else if(is_temporal_operator(op)) { throw ebmc_errort() << "failed to make NNF for " << op.id(); @@ -530,6 +535,23 @@ static obligationst property_obligations_rec( instantiate_property(property_expr, current, no_timeframes)}; } } + else if(property_expr.id() == ID_sva_implies) + { + // We need NNF, hence we go via implies_exprt. + // Note that this is not an SVA sequence operator. + auto &sva_implies_expr = to_sva_implies_expr(property_expr); + auto implies_expr = + implies_exprt{sva_implies_expr.lhs(), sva_implies_expr.rhs()}; + return property_obligations_rec(implies_expr, current, no_timeframes); + } + else if(property_expr.id() == ID_sva_iff) + { + // We need NNF, hence we go via equal_exprt. + // Note that this is not an SVA sequence operator. + auto &sva_iff_expr = to_sva_iff_expr(property_expr); + auto equal_expr = equal_exprt{sva_iff_expr.lhs(), sva_iff_expr.rhs()}; + return property_obligations_rec(equal_expr, current, no_timeframes); + } else { return obligationst{ @@ -549,6 +571,26 @@ Function: property_obligations \*******************************************************************/ +obligationst property_obligations( + const exprt &property_expr, + const mp_integer &t, + const mp_integer &no_timeframes) +{ + return property_obligations_rec(property_expr, t, no_timeframes); +} + +/*******************************************************************\ + +Function: property_obligations + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + obligationst property_obligations( const exprt &property_expr, const mp_integer &no_timeframes) diff --git a/src/trans-word-level/property.h b/src/trans-word-level/property.h index 2b9f576f4..1bff3522b 100644 --- a/src/trans-word-level/property.h +++ b/src/trans-word-level/property.h @@ -42,4 +42,11 @@ symbol_exprt lasso_symbol(const mp_integer &k, const mp_integer &i); /// Returns true iff the given property requires lasso constraints for BMC. bool requires_lasso_constraints(const exprt &); +class obligationst; + +obligationst property_obligations( + const exprt &, + const mp_integer &t, + const mp_integer &no_timeframes); + #endif diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index eddc13cc7..3f4f0e73c 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -12,7 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "instantiate_word_level.h" +#include "obligations.h" +#include "property.h" std::vector> instantiate_sequence( exprt expr, @@ -153,13 +154,14 @@ std::vector> instantiate_sequence( // 3. The end time of the composite sequence is // the end time of the operand sequence that completes last. // Condition (3) is TBD. - exprt::operandst conjuncts; + obligationst obligations; for(auto &op : expr.operands()) - conjuncts.push_back(instantiate_property(op, t, no_timeframes).second); + { + obligations.add(property_obligations(op, t, no_timeframes)); + } - exprt condition = conjunction(conjuncts); - return {{t, condition}}; + return {obligations.conjunction()}; } else if(expr.id() == ID_sva_or) { @@ -177,6 +179,7 @@ std::vector> instantiate_sequence( else { // not a sequence, evaluate as state predicate - return {instantiate_property(expr, t, no_timeframes)}; + auto obligations = property_obligations(expr, t, no_timeframes); + return {obligations.conjunction()}; } }