SVA: bugfix for sequence implication operators

The sequence implication operators |-> and |=> are property expressions, and
not sequence expressions.

Furthermore, the implication must hold for _all_ matches of the LHS
sequence; a single one is not sufficient.

Author: kroening

CHANGELOG

@@ -4,6 +4,7 @@
 * SystemVerilog: assignment patterns with keys for structs
 * SystemVerilog: unbased unsigned literals '0, '1, 'x, 'z
 * SystemVerilog: first_match
+* SystemVerilog: bugfix for |-> and |=>
 * Verilog: 'dx, 'dz
 * SMV: LTL V operator, xnor operator
 * SMV: word types and operators

regression/verilog/SVA/sequence_first_match2.desc

@@ -1,11 +1,11 @@
 CORE
 sequence_first_match2.sv
 --bound 5
-^\[.*\] \(\(##1 1\) or \(##2 1\)\) \|-> main.x == 1: PROVED up to bound 5$
+^\[.*\] \(\(##1 1\) or \(##2 1\)\) \|-> main.x == 1: REFUTED$
 ^\[.*\] first_match\(\(##1 1\) or \(##2 1\)\) \|-> main\.x == 1: PROVED up to bound 5$
-^\[.*\] \(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED up to bound 5$
+^\[.*\] \(1 or \(##1 1\)\) \|-> main\.x == 0: REFUTED$
 ^\[.*\] first_match\(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED up to bound 5$
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/SVA/sequence_implication1.desc

@@ -1,7 +1,11 @@
 CORE
 sequence_implication1.sv
 --bound 20
-^EXIT=0$
+^\[.*\] always \(\(main\.counter == 1 ##1 main\.counter == 2\) \|-> \(##1 main.counter == 0\)\): PROVED up to bound 20$
+^\[.*\] always \(\(main\.counter == 1 ##1 main\.counter == 2\) \|=> main\.counter == 0\): PROVED up to bound 20$
+^\[.*\] always \(0 \|-> 0\): PROVED up to bound 20$
+^\[.*\] \(1 or \(##1 1\)\) \|-> main\.counter == 0: REFUTED$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/SVA/sequence_implication1.sv

@@ -15,4 +15,10 @@ module main(input clk);
   // same with non-overlapping implication
   assert property (@(posedge clk) counter == 1 ##1 counter == 2 |=> counter == 0);
 
+  // if the LHS doesn't match the implication is vacuously true
+  assert property (0 |-> 0);
+
+  // the implication must hold for _all_ matches of the LHS, not just one
+  initial assert property (1 or ##1 1 |-> counter==0);
+
 endmodule : main

src/temporal-logic/temporal_logic.cpp

@@ -95,12 +95,11 @@ bool is_LTL_past(const exprt &expr)
 bool is_SVA_sequence_operator(const exprt &expr)
 {
   auto id = expr.id();
-  // Note that ID_sva_overlapped_followed_by and ID_sva_nonoverlapped_followed_by
+  // Note that ID_sva_overlapped_followed_by, ID_sva_nonoverlapped_followed_by,
+  // ID_sva_non_overlapped_implication and ID_sva_overlapped_implication
   // are property expressions, not sequence expressions.
   // Note that ID_sva_not does not yield a sequence expression.
-  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 ||
+  return id == ID_sva_and || id == ID_sva_or || id == ID_sva_cycle_delay ||
          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 ||
@@ -124,6 +123,8 @@ bool is_SVA_operator(const exprt &expr)
          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_implication ||
+         id == ID_sva_non_overlapped_implication ||
          id == ID_sva_overlapped_followed_by ||
          id == ID_sva_nonoverlapped_followed_by;
 }

src/trans-word-level/property.cpp

@@ -576,6 +576,48 @@ static obligationst property_obligations_rec(
     auto equal_expr = equal_exprt{sva_iff_expr.lhs(), sva_iff_expr.rhs()};
     return property_obligations_rec(equal_expr, current, no_timeframes);
   }
+  else if(
+    property_expr.id() == ID_sva_overlapped_implication ||
+    property_expr.id() == ID_sva_non_overlapped_implication)
+  {
+    auto &implication = to_binary_expr(property_expr);
+
+    // The LHS is a sequence, the RHS is a property.
+    // The implication must hold for _all_ matches on the LHS,
+    // i.e., each pair of LHS match and RHS obligation yields an obligation.
+    const auto lhs_match_points =
+      instantiate_sequence(implication.lhs(), current, no_timeframes);
+
+    obligationst result;
+
+    for(auto &lhs_match_point : lhs_match_points)
+    {
+      // The RHS of the non-overlapped implication starts one timeframe later
+      auto t_rhs = property_expr.id() == ID_sva_non_overlapped_implication
+                     ? lhs_match_point.first + 1
+                     : lhs_match_point.first;
+
+      // Do we exceed the bound? Make it 'true'
+      if(t_rhs >= no_timeframes)
+      {
+        DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
+        return obligationst{no_timeframes - 1, true_exprt()};
+      }
+
+      // Get obligations for RHS
+      auto rhs_obligations_rec =
+        property_obligations_rec(implication.rhs(), t_rhs, no_timeframes);
+
+      for(auto &rhs_obligation : rhs_obligations_rec.map)
+      {
+        auto rhs_conjunction = conjunction(rhs_obligation.second);
+        auto cond = implies_exprt{lhs_match_point.second, rhs_conjunction};
+        result.add(rhs_obligation.first, cond);
+      }
+    }
+
+    return result;
+  }
   else if(
     property_expr.id() == ID_sva_nonoverlapped_followed_by ||
     property_expr.id() == ID_sva_overlapped_followed_by)

src/trans-word-level/sequence.cpp

@@ -75,23 +75,18 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
       return match_points;
     }
   }
-  else if(
-    expr.id() == ID_sva_sequence_concatenation ||
-    expr.id() == ID_sva_overlapped_implication ||
-    expr.id() == ID_sva_non_overlapped_implication)
+  else if(expr.id() == ID_sva_sequence_concatenation)
   {
     auto &implication = to_binary_expr(expr);
     std::vector<std::pair<mp_integer, exprt>> result;
 
     // This is the product of the match points on the LHS and RHS
     const auto lhs_match_points =
       instantiate_sequence(implication.lhs(), t, no_timeframes);
+
     for(auto &lhs_match_point : lhs_match_points)
     {
-      // The RHS of the non-overlapped implication starts one timeframe later
-      auto t_rhs = expr.id() == ID_sva_non_overlapped_implication
-                     ? lhs_match_point.first + 1
-                     : lhs_match_point.first;
+      auto t_rhs = lhs_match_point.first;
 
       // Do we exceed the bound? Make it 'true'
       if(t_rhs >= no_timeframes)
@@ -105,20 +100,7 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
 
       for(auto &rhs_match_point : rhs_match_points)
       {
-        exprt cond;
-        if(expr.id() == ID_sva_sequence_concatenation)
-        {
-          cond = and_exprt{lhs_match_point.second, rhs_match_point.second};
-        }
-        else if(
-          expr.id() == ID_sva_overlapped_implication ||
-          expr.id() == ID_sva_non_overlapped_implication)
-        {
-          cond = implies_exprt{lhs_match_point.second, rhs_match_point.second};
-        }
-        else
-          PRECONDITION(false);
-
+        auto cond = and_exprt{lhs_match_point.second, rhs_match_point.second};
         result.push_back({rhs_match_point.first, cond});
       }
     }