SVA to LTL now converts SVA sequences

This adds support for mapping some SVA sequences to equivalent LTL.

Author: kroening

regression/ebmc/smv-netlist/cycle_delay1.desc

@@ -0,0 +1,7 @@
+CORE
+cycle_delay1.sv
+--smv-netlist
+^LTLSPEC node22 & X node25 & X X node28 & X X X node31$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-netlist/cycle_delay1.sv

@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg [3:0] x = 0;
+
+  always_ff @(posedge clk)
+    x++;
+
+  initial assert property (x == 0 ##1 x == 1 ##1 x == 2 ##1 x == 3);
+
+endmodule

src/temporal-logic/temporal_logic.cpp

@@ -224,6 +224,85 @@ static exprt n_Xes(mp_integer n, exprt op)
     return n_Xes(n - 1, X_exprt{std::move(op)});
 }
 
+// Returns a set of match conditions (given as LTL formula)
+struct ltl_sequence_matcht
+{
+  ltl_sequence_matcht(exprt __cond, mp_integer __length)
+    : cond(std::move(__cond)), length(std::move(__length))
+  {
+    PRECONDITION(length >= 0);
+  }
+
+  exprt cond;        // LTL
+  mp_integer length; // match_end - match_start + 1
+
+  bool empty() const
+  {
+    return length == 0;
+  }
+};
+
+std::vector<ltl_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
+{
+  if(!is_SVA_sequence_operator(sequence))
+  {
+    // atomic proposition
+    return {{sequence, 1}};
+  }
+  else if(sequence.id() == ID_sva_sequence_concatenation)
+  {
+    auto &concatenation = to_sva_sequence_concatenation_expr(sequence);
+    auto matches_lhs = LTL_sequence_matches(concatenation.lhs());
+    auto matches_rhs = LTL_sequence_matches(concatenation.rhs());
+
+    if(matches_lhs.empty() || matches_rhs.empty())
+      return {};
+
+    std::vector<ltl_sequence_matcht> result;
+    // cross product
+    for(auto &match_lhs : matches_lhs)
+      for(auto &match_rhs : matches_rhs)
+      {
+        // Concatenation is overlapping, hence deduct one from
+        // the length.
+        auto delay = match_lhs.length - 1;
+        auto rhs_delayed = n_Xes(delay, match_rhs.cond);
+        result.emplace_back(
+          and_exprt{match_lhs.cond, rhs_delayed},
+          match_lhs.length + match_rhs.length - 1);
+      }
+    return result;
+  }
+  else if(sequence.id() == ID_sva_cycle_delay)
+  {
+    auto &delay = to_sva_cycle_delay_expr(sequence);
+    auto matches = LTL_sequence_matches(delay.op());
+    auto from_int = numeric_cast_v<mp_integer>(delay.from());
+
+    if(matches.empty())
+      return {};
+
+    if(delay.to().is_nil())
+    {
+      for(auto &match : matches)
+      {
+        // delay as instructed
+        match.length += from_int;
+        match.cond = n_Xes(from_int, match.cond);
+      }
+      return matches;
+    }
+    else
+      return {};
+  }
+  else
+  {
+    return {}; // unsupported
+  }
+}
+
+/// takes an SVA property as input, and returns an equivalent LTL property,
+/// or otherwise {}.
 std::optional<exprt> SVA_to_LTL(exprt expr)
 {
   // Some SVA is directly mappable to LTL
@@ -317,25 +396,104 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     else
       return {};
   }
-  else if(expr.id() == ID_sva_overlapped_implication)
+  else if(
+    expr.id() == ID_sva_overlapped_implication ||
+    expr.id() == ID_sva_non_overlapped_implication)
   {
-    auto &implication = to_sva_overlapped_implication_expr(expr);
-    auto rec_lhs = SVA_to_LTL(implication.lhs());
-    auto rec_rhs = SVA_to_LTL(implication.rhs());
-    if(rec_lhs.has_value() && rec_rhs.has_value())
-      return implies_exprt{rec_lhs.value(), rec_rhs.value()};
-    else
+    auto &implication = to_sva_implication_base_expr(expr);
+    auto matches = LTL_sequence_matches(implication.sequence());
+
+    if(matches.empty())
       return {};
+
+    // All matches must be followed
+    // by the property being true
+    exprt::operandst conjuncts;
+
+    auto property_rec = SVA_to_LTL(implication.property());
+
+    if(!property_rec.has_value())
+      return {};
+
+    for(auto &match : matches)
+    {
+      const auto overlapped = expr.id() == ID_sva_overlapped_implication;
+      if(match.empty() && overlapped)
+      {
+        // ignore the empty match
+      }
+      else
+      {
+        auto delay = match.length + (overlapped ? 0 : 1) - 1;
+        auto delayed_property = n_Xes(delay, property_rec.value());
+        conjuncts.push_back(implies_exprt{match.cond, delayed_property});
+      }
+    }
+
+    return conjunction(conjuncts);
   }
-  else if(expr.id() == ID_sva_non_overlapped_implication)
+  else if(
+    expr.id() == ID_sva_nonoverlapped_followed_by ||
+    expr.id() == ID_sva_overlapped_followed_by)
   {
-    auto &implication = to_sva_non_overlapped_implication_expr(expr);
-    auto rec_lhs = SVA_to_LTL(implication.lhs());
-    auto rec_rhs = SVA_to_LTL(implication.rhs());
-    if(rec_lhs.has_value() && rec_rhs.has_value())
-      return implies_exprt{rec_lhs.value(), X_exprt{rec_rhs.value()}};
-    else
+    auto &followed_by = to_sva_followed_by_expr(expr);
+    auto matches = LTL_sequence_matches(followed_by.sequence());
+
+    if(matches.empty())
+      return {};
+
+    // There must be at least one match that is followed
+    // by the property being true
+    exprt::operandst disjuncts;
+
+    auto property_rec = SVA_to_LTL(followed_by.property());
+
+    if(!property_rec.has_value())
       return {};
+
+    for(auto &match : matches)
+    {
+      const auto overlapped = expr.id() == ID_sva_overlapped_followed_by;
+      if(match.empty() && overlapped)
+      {
+        // ignore the empty match
+      }
+      else
+      {
+        auto delay = match.length + (overlapped ? 0 : 1) - 1;
+        auto delayed_property = n_Xes(delay, property_rec.value());
+        disjuncts.push_back(and_exprt{match.cond, delayed_property});
+      }
+    }
+
+    return disjunction(disjuncts);
+  }
+  else if(expr.id() == ID_sva_sequence_property)
+  {
+    // should have been turned into sva_implicit_weak or sva_implicit_strong
+    PRECONDITION(false);
+  }
+  else if(
+    expr.id() == ID_sva_weak || expr.id() == ID_sva_strong ||
+    expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong)
+  {
+    auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
+
+    // evaluates to true if there's at least one non-empty match of the sequence
+    auto matches = LTL_sequence_matches(sequence);
+
+    if(matches.empty())
+      return {};
+
+    exprt::operandst disjuncts;
+
+    for(auto &match : matches)
+    {
+      if(!match.empty())
+        disjuncts.push_back(match.cond);
+    }
+
+    return disjunction(disjuncts);
   }
   else if(!has_temporal_operator(expr))
   {

src/verilog/sva_expr.h

@@ -663,6 +663,16 @@ class sva_implication_base_exprt : public binary_predicate_exprt
     return lhs();
   }
 
+  const exprt &sequence() const
+  {
+    return op0();
+  }
+
+  exprt &sequence()
+  {
+    return op0();
+  }
+
   // a property
   const exprt &consequent() const
   {
@@ -673,8 +683,32 @@ class sva_implication_base_exprt : public binary_predicate_exprt
   {
     return rhs();
   }
+
+  const exprt &property() const
+  {
+    return op1();
+  }
+
+  exprt &property()
+  {
+    return op1();
+  }
 };
 
+static inline const sva_implication_base_exprt &
+to_sva_implication_base_expr(const exprt &expr)
+{
+  sva_implication_base_exprt::check(expr);
+  return static_cast<const sva_implication_base_exprt &>(expr);
+}
+
+static inline sva_implication_base_exprt &
+to_sva_implication_base_expr(exprt &expr)
+{
+  sva_implication_base_exprt::check(expr);
+  return static_cast<sva_implication_base_exprt &>(expr);
+}
+
 /// |->
 class sva_overlapped_implication_exprt : public sva_implication_base_exprt
 {