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

src/temporal-logic/temporal_logic.cpp

@@ -10,6 +10,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/expr_util.h>
 
+#include <verilog/sva_expr.h>
+
+#include "ltl.h"
+
 bool is_temporal_operator(const exprt &expr)
 {
   return is_CTL_operator(expr) || is_LTL_operator(expr) ||
@@ -136,3 +140,78 @@ bool is_SVA(const exprt &expr)
 
   return !has_subexpr(expr, non_SVA_operator);
 }
+
+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 {};
+}

src/temporal-logic/temporal_logic.h

@@ -71,4 +71,8 @@ bool is_SVA_operator(const exprt &);
 /// Returns true iff the given expression is an SVA expression
 bool is_SVA(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