smv-netlist: use expr2smv for property

The SMV to netlist conversion now uses expr2smv for outputting the property,
which enables outputting full LTL or CTL.

Author: kroening

regression/ebmc/smv-netlist/smv1.desc

@@ -0,0 +1,10 @@
+CORE
+smv1.smv
+--smv-netlist
+^MODULE main$
+^VAR smv\.main\.var\.x: boolean;$
+^ASSIGN next\(smv\.main\.var\.x\):=\!smv\.main\.var\.x;$
+^INIT !smv\.main\.var\.x$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-netlist/smv1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x: boolean;
+
+ASSIGN next(x):=!x;
+ASSIGN init(x):=FALSE;
+
+LTLSPEC G F x
+

regression/ebmc/smv-netlist/verilog1.desc

@@ -0,0 +1,11 @@
+CORE
+verilog1.sv
+--smv-netlist
+^MODULE main$
+^VAR Verilog\.main\.x: boolean;$
+^ASSIGN next\(Verilog\.main\.x\):=\!Verilog\.main\.x;$
+^INIT !Verilog\.main\.x$
+^LTLSPEC G F Verilog\.main\.x$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-netlist/verilog1.sv

@@ -0,0 +1,12 @@
+module main(input clk);
+
+  reg x;
+
+  initial x = 0;
+
+  always @(posedge clk)
+    x = !x;
+
+  always assert property (always s_eventually x);
+
+endmodule

src/ebmc/bdd_engine.cpp

@@ -1054,12 +1054,10 @@ void bdd_enginet::build_BDDs()
         auto netlist_property = netlist.properties.find(property.identifier);
         CHECK_RETURN(netlist_property != netlist.properties.end());
         DATA_INVARIANT(
-          netlist_property->second.id() == ID_sva_always,
-          "assumed property must be sva_always");
-        auto &p = to_sva_always_expr(netlist_property->second).op();
+          netlist_property->second.id() == ID_G, "assumed property must be G");
+        auto &p = to_G_expr(netlist_property->second).op();
         DATA_INVARIANT(
-          p.id() == ID_literal,
-          "assumed property must be sva_assume sva_assert literal");
+          p.id() == ID_literal, "assumed property must be G literal");
         auto l = to_literal_expr(p).get_literal();
         constraints_BDDs.push_back(aig2bdd(l, BDDs));
       }

src/trans-netlist/instantiate_netlist.cpp

@@ -311,20 +311,10 @@ std::optional<exprt> netlist_property(
     }
     else if(is_SVA_operator(expr))
     {
-      if(expr.id() == ID_sva_always || expr.id() == ID_sva_assume)
-      {
-        auto copy = expr;
-        auto &op = to_unary_expr(copy).op();
-        auto op_opt =
-          netlist_property(solver, var_map, op, ns, message_handler);
-        if(op_opt.has_value())
-        {
-          op = op_opt.value();
-          return copy;
-        }
-        else
-          return {};
-      }
+      // Try to turn into LTL
+      auto LTL_opt = SVA_to_LTL(expr);
+      if(LTL_opt.has_value())
+        return netlist_property(solver, var_map, *LTL_opt, ns, message_handler);
       else
         return {};
     }

src/trans-netlist/smv_netlist.cpp

@@ -88,21 +88,35 @@ void print_smv(const netlistt &netlist, std::ostream &out, const exprt &expr)
   symbol_tablet symbol_table;
   namespacet ns{symbol_table};
 
-  // replace literal expressions by symbols
+  class expr2smv_netlistt : public expr2smvt
+  {
+  public:
+    expr2smv_netlistt(const namespacet &ns, const netlistt &__netlist)
+      : expr2smvt(ns), netlist(__netlist)
+    {
+    }
+
+  protected:
+    const netlistt &netlist;
 
-  exprt replaced = expr;
-  replaced.visit_pre(
-    [&netlist](exprt &node)
+    resultt convert_rec(const exprt &expr) override
     {
-      if(node.id() == ID_literal)
+      if(expr.id() == ID_literal)
       {
         std::ostringstream buffer;
-        print_smv(netlist, buffer, to_literal_expr(node).get_literal());
-        node = symbol_exprt{buffer.str(), node.type()};
+        auto l = to_literal_expr(expr).get_literal();
+        print_smv(netlist, buffer, l);
+        if(l.sign())
+          return {precedencet::NOT, buffer.str()};
+        else
+          return {precedencet::MAX, buffer.str()};
       }
-    });
+      else
+        return expr2smvt::convert_rec(expr);
+    }
+  };
 
-  out << expr2smv(replaced, ns);
+  out << expr2smv_netlistt{ns, netlist}.convert(expr);
 }
 
 void smv_netlist(const netlistt &netlist, std::ostream &out)
@@ -243,29 +257,8 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
     }
     else if(is_SVA(netlist_expr))
     {
-      if(is_SVA_always_p(netlist_expr))
-      {
-        out << "-- " << id << '\n';
-        out << "CTLSPEC AG ";
-        print_smv(netlist, out, to_sva_always_expr(netlist_expr).op());
-        out << '\n';
-      }
-      else if(is_SVA_always_s_eventually_p(netlist_expr))
-      {
-        out << "-- " << id << '\n';
-        out << "CTLSPEC AG AF ";
-        print_smv(
-          netlist,
-          out,
-          to_sva_s_eventually_expr(to_sva_always_expr(netlist_expr).op()).op());
-        out << '\n';
-      }
-      else
-      {
-        out << "-- " << id << '\n';
-        out << "-- not translated\n";
-        out << '\n';
-      }
+      // Should have been mapped to LTL
+      DATA_INVARIANT(false, "smv_netlist got SVA");
     }
     else
     {