extract SVA_to_LTL(exprt) into a separate file

src/temporal-logic/Makefile

@@ -2,6 +2,7 @@ SRC = ctl.cpp \
       ltl.cpp \
       nnf.cpp \
       normalize_property.cpp \
+      sva_to_ltl.cpp \
       temporal_logic.cpp \
       trivial_sva.cpp \
       #empty line

src/temporal-logic/sva_to_ltl.cpp

@@ -0,0 +1,359 @@
+/*******************************************************************\
+
+Module: SVA to LTL
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <util/arith_tools.h>
+
+#include <verilog/sva_expr.h>
+
+#include "ltl.h"
+#include "temporal_logic.h"
+
+static exprt n_Xes(mp_integer n, exprt op)
+{
+  PRECONDITION(n >= 0);
+  if(n == 0)
+    return op;
+  else
+    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 if(delay.to().id() == ID_infinity)
+    {
+      return {}; // can't encode
+    }
+    else if(delay.to().is_constant())
+    {
+      auto to_int = numeric_cast_v<mp_integer>(to_constant_expr(delay.to()));
+      std::vector<ltl_sequence_matcht> new_matches;
+
+      for(mp_integer i = from_int; i <= to_int; ++i)
+      {
+        for(const auto &match : matches)
+        {
+          // delay as instructed
+          auto new_match = match;
+          new_match.length += from_int;
+          new_match.cond = n_Xes(i, match.cond);
+          new_matches.push_back(std::move(new_match));
+        }
+      }
+
+      return new_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
+  if(expr.id() == ID_sva_always)
+  {
+    auto rec = SVA_to_LTL(to_sva_always_expr(expr).op());
+    if(rec.has_value())
+      return G_exprt{rec.value()};
+    else
+      return {};
+  }
+  else if(expr.id() == ID_sva_ranged_always)
+  {
+    auto &ranged_always = to_sva_ranged_always_expr(expr);
+    auto rec = SVA_to_LTL(ranged_always.op());
+    if(rec.has_value())
+    {
+      // always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
+      auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
+
+      // Is there an upper end of the range?
+      if(ranged_always.upper().is_constant())
+      {
+        // upper end set
+        auto upper_int =
+          numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.upper()));
+        PRECONDITION(upper_int >= lower_int);
+        auto diff = upper_int - lower_int;
+
+        exprt::operandst conjuncts;
+
+        for(auto i = 0; i <= diff; i++)
+          conjuncts.push_back(n_Xes(i, rec.value()));
+
+        return n_Xes(lower_int, conjunction(conjuncts));
+      }
+      else if(ranged_always.upper().id() == ID_infinity)
+      {
+        // always [l:$] op ---> X ... X G op
+        return n_Xes(lower_int, G_exprt{rec.value()});
+      }
+      else
+        PRECONDITION(false);
+    }
+    else
+      return {};
+  }
+  else if(expr.id() == ID_sva_s_always)
+  {
+    auto &ranged_always = to_sva_s_always_expr(expr);
+    auto rec = SVA_to_LTL(ranged_always.op());
+    if(rec.has_value())
+    {
+      // s_always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
+      auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
+      auto upper_int = numeric_cast_v<mp_integer>(ranged_always.upper());
+      PRECONDITION(upper_int >= lower_int);
+      auto diff = upper_int - lower_int;
+
+      exprt::operandst conjuncts;
+
+      for(auto i = 0; i <= diff; i++)
+        conjuncts.push_back(n_Xes(i, rec.value()));
+
+      return n_Xes(lower_int, conjunction(conjuncts));
+    }
+    else
+      return {};
+  }
+  else if(expr.id() == ID_sva_s_eventually)
+  {
+    auto rec = SVA_to_LTL(to_sva_s_eventually_expr(expr).op());
+    if(rec.has_value())
+      return F_exprt{rec.value()};
+    else
+      return {};
+  }
+  else if(expr.id() == ID_sva_s_nexttime)
+  {
+    auto rec = SVA_to_LTL(to_sva_s_nexttime_expr(expr).op());
+    if(rec.has_value())
+      return X_exprt{rec.value()};
+    else
+      return {};
+  }
+  else if(expr.id() == ID_sva_nexttime)
+  {
+    auto rec = SVA_to_LTL(to_sva_nexttime_expr(expr).op());
+    if(rec.has_value())
+      return X_exprt{rec.value()};
+    else
+      return {};
+  }
+  else if(
+    expr.id() == ID_sva_overlapped_implication ||
+    expr.id() == ID_sva_non_overlapped_implication)
+  {
+    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_nonoverlapped_followed_by ||
+    expr.id() == ID_sva_overlapped_followed_by)
+  {
+    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(expr.id() == ID_sva_s_until)
+  {
+    auto &until = to_sva_s_until_expr(expr);
+    auto rec_lhs = SVA_to_LTL(until.lhs());
+    auto rec_rhs = SVA_to_LTL(until.rhs());
+    if(rec_lhs.has_value() && rec_rhs.has_value())
+      return U_exprt{rec_lhs.value(), rec_rhs.value()};
+    else
+      return {};
+  }
+  else if(expr.id() == ID_sva_s_until_with)
+  {
+    // This is release with swapped operands
+    auto &until_with = to_sva_s_until_with_expr(expr);
+    auto rec_lhs = SVA_to_LTL(until_with.lhs());
+    auto rec_rhs = SVA_to_LTL(until_with.rhs());
+    if(rec_lhs.has_value() && rec_rhs.has_value())
+      return R_exprt{rec_rhs.value(), rec_lhs.value()}; // swapped
+    else
+      return {};
+  }
+  else if(!has_temporal_operator(expr))
+  {
+    return expr;
+  }
+  else if(
+    expr.id() == ID_and || expr.id() == ID_implies || expr.id() == ID_or ||
+    expr.id() == ID_not)
+  {
+    for(auto &op : expr.operands())
+    {
+      auto rec = SVA_to_LTL(op);
+      if(!rec.has_value())
+        return {};
+      op = rec.value();
+    }
+    return expr;
+  }
+  else
+    return {};
+}