Merge pull request #767 from diffblue/change-Fphi-encoding

change Fφ BMC encoding

Author: kroening

regression/verilog/SVA/eventually4.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 eventually4.sv
 --bound 2
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Property gives counterexample but should pass.

regression/verilog/SVA/sva_iff2.sv

@@ -1,8 +1,8 @@
 module main(input a, b);
 
-  // p0: assert property ((always a) iff (always a));
+  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));
+  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));

regression/verilog/SVA/sva_implies2.desc

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

regression/verilog/SVA/sva_implies2.sv

@@ -0,0 +1,12 @@
+module main(input a, b);
+
+  p0: assert property ((always a) implies (always a));
+  p1: assert property ((a or (always b)) implies (a or (always b)));
+  p2: assert property ((eventually[0:1] a) implies (eventually[0:1] a));
+  p3: assert property ((s_eventually a) implies (s_eventually a));
+  p4: assert property ((a until b) implies (a until b));
+  // p5: assert property ((a s_until b) implies (a s_until a));
+  p6: assert property ((a until_with b) implies (a until_with b));
+  p7: assert property ((a s_until_with b) implies (a s_until_with a));
+
+endmodule

src/temporal-logic/normalize_property.cpp

@@ -91,8 +91,8 @@ exprt normalize_property_rec(exprt expr)
   }
   else if(expr.id() == ID_sva_cycle_delay_plus)
   {
-    expr = sva_s_eventually_exprt{
-      sva_s_nexttime_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
+    expr = sva_s_nexttime_exprt{
+      sva_s_eventually_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
   }
   else if(expr.id() == ID_sva_cycle_delay_star)
   {

src/trans-word-level/property.cpp

@@ -256,6 +256,19 @@ static obligationst property_obligations_rec(
 
     obligationst obligations;
 
+    // Traces with any φ state from "current" onwards satisfy Fφ
+    exprt::operandst phi_disjuncts;
+
+    phi_disjuncts.reserve(numeric_cast_v<std::size_t>(no_timeframes - current));
+
+    for(mp_integer j = current; j < no_timeframes; ++j)
+    {
+      auto tmp = property_obligations_rec(phi, j, no_timeframes);
+      phi_disjuncts.push_back(tmp.conjunction().second);
+    }
+
+    auto phi_disjunction = disjunction(phi_disjuncts);
+
     // Counterexamples to Fφ must have a loop.
     // We consider l-k loops with l<k.
     for(mp_integer k = current + 1; k < no_timeframes; ++k)
@@ -265,19 +278,13 @@ static obligationst property_obligations_rec(
       //
       // (1) There is a loop from timeframe k back to
       //     some earlier state l with current<=l<k.
-      // (2) No state j with current<=j<=k to the end of the
-      //     lasso satisfies 'φ'.
+      // (2) No state j with current<=j<no_timeframes satisfies 'φ'.
+      //     The weaker alternative current<=j<=k yields counterexamples
+      //     that exhibit a ¬φ loop, but are then followed by a φ state.
       for(mp_integer l = current; l < k; ++l)
       {
-        exprt::operandst disjuncts = {not_exprt(lasso_symbol(l, k))};
-
-        for(mp_integer j = current; j <= k; ++j)
-        {
-          auto tmp = property_obligations_rec(phi, j, no_timeframes);
-          disjuncts.push_back(tmp.conjunction().second);
-        }
-
-        obligations.add(k, disjunction(disjuncts));
+        auto tmp = or_exprt{not_exprt(lasso_symbol(l, k)), phi_disjunction};
+        obligations.add(k, std::move(tmp));
       }
     }