SMV netlist: translate some SVA to LTL

Parts of SVA map directly to LTL.  This allows extending the set of formulas
converted to LTL when outputting an SMV model.

Author: kroening

Diff for: src/temporal-logic/temporal_logic.cpp

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <verilog/sva_expr.h>
 
+#include "ltl.h"
+
 bool is_temporal_operator(const exprt &expr)
 {
   return is_CTL_operator(expr) || is_LTL_operator(expr) ||
@@ -152,3 +154,78 @@ bool is_SVA_always_s_eventually_p(const exprt &expr)
          !has_temporal_operator(
            to_sva_s_eventually_expr(to_sva_always_expr(expr).op()).op());
 }
+
+std::optional<exprt> SVA_to_LTL(const 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_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)
+  {
+    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
+      return {};
+  }
+  else if(expr.id() == ID_sva_non_overlapped_implication)
+  {
+    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
+      return {};
+  }
+  else if(
+    expr.id() == ID_and || expr.id() == ID_implies || expr.id() == ID_or ||
+    expr.id() == ID_not)
+  {
+    exprt copy = expr;
+    for(auto &op : copy.operands())
+    {
+      auto rec = SVA_to_LTL(op);
+      if(!rec.has_value())
+        return {};
+      op = rec.value();
+    }
+    return copy;
+  }
+  else if(!has_temporal_operator(expr))
+    return expr;
+  else
+    return {};
+}

Diff for: src/temporal-logic/temporal_logic.h

@@ -77,4 +77,8 @@ bool is_SVA_always_p(const exprt &);
 /// Returns true iff the given expression is always s_eventually p
 bool is_SVA_always_s_eventually_p(const exprt &);
 
+/// If possible, this maps an SVA expression to an equivalent LTL
+/// expression, or otherwise returns {}.
+std::optional<exprt> SVA_to_LTL(const exprt &);
+
 #endif