Merge pull request #743 from diffblue/sva_and_or_property

word-level BMC: allow SVA and/or/implies/iff at property level

Author: kroening

regression/verilog/SVA/sva_iff2.desc

@@ -0,0 +1,8 @@
+CORE
+sva_iff2.sv
+--bound 10
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

src/temporal-logic/nnf.cpp

@@ -68,6 +68,23 @@ std::optional<exprt> 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 ¬ψ)

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)

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

src/trans-word-level/sequence.cpp

@@ -12,7 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <verilog/sva_expr.h>
 
-#include "instantiate_word_level.h"
+#include "obligations.h"
+#include "property.h"
 
 std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
   exprt expr,
@@ -153,13 +154,14 @@ std::vector<std::pair<mp_integer, exprt>> 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<std::pair<mp_integer, exprt>> 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()};
   }
 }