Merge pull request #1058 from diffblue/smv_netlist2

smv-netlist: use expr2smv for property

Author: tautschnig

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

@@ -20,7 +20,7 @@ std::string id2smv(const irep_idt &id)
 {
   std::string result;
 
-  for(unsigned i = 0; i < id.size(); i++)
+  for(std::size_t i = 0; i < id.size(); i++)
   {
     const bool first = i == 0;
     char ch = id[i];
@@ -60,7 +60,7 @@ void print_smv(const netlistt &netlist, std::ostream &out, literalt a)
     return;
   }
 
-  unsigned node_nr = a.var_no();
+  std::size_t node_nr = a.var_no();
   DATA_INVARIANT(node_nr < netlist.number_of_nodes(), "node_nr in range");
 
   if(a.sign())
@@ -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)
@@ -115,17 +129,15 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
 
   auto &var_map = netlist.var_map;
 
-  for(var_mapt::mapt::const_iterator it = var_map.map.begin();
-      it != var_map.map.end();
-      it++)
+  for(auto &var_it : var_map.map)
   {
-    const var_mapt::vart &var = it->second;
+    const var_mapt::vart &var = var_it.second;
 
-    for(unsigned i = 0; i < var.bits.size(); i++)
+    for(std::size_t i = 0; i < var.bits.size(); i++)
     {
       if(var.is_latch())
       {
-        out << "VAR " << id2smv(it->first);
+        out << "VAR " << id2smv(var_it.first);
         if(var.bits.size() != 1)
           out << "[" << i << "]";
         out << ": boolean;" << '\n';
@@ -137,17 +149,15 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
   out << "-- Inputs" << '\n';
   out << '\n';
 
-  for(var_mapt::mapt::const_iterator it = var_map.map.begin();
-      it != var_map.map.end();
-      it++)
+  for(auto &var_it : var_map.map)
   {
-    const var_mapt::vart &var = it->second;
+    const var_mapt::vart &var = var_it.second;
 
-    for(unsigned i = 0; i < var.bits.size(); i++)
+    for(std::size_t i = 0; i < var.bits.size(); i++)
     {
       if(var.is_input())
       {
-        out << "VAR " << id2smv(it->first);
+        out << "VAR " << id2smv(var_it.first);
         if(var.bits.size() != 1)
           out << "[" << i << "]";
         out << ": boolean;" << '\n';
@@ -161,7 +171,7 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
 
   auto &nodes = netlist.nodes;
 
-  for(unsigned node_nr = 0; node_nr < nodes.size(); node_nr++)
+  for(std::size_t node_nr = 0; node_nr < nodes.size(); node_nr++)
   {
     const aig_nodet &node = nodes[node_nr];
 
@@ -179,17 +189,15 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
   out << "-- Next state functions" << '\n';
   out << '\n';
 
-  for(var_mapt::mapt::const_iterator it = var_map.map.begin();
-      it != var_map.map.end();
-      it++)
+  for(auto &var_it : var_map.map)
   {
-    const var_mapt::vart &var = it->second;
+    const var_mapt::vart &var = var_it.second;
 
-    for(unsigned i = 0; i < var.bits.size(); i++)
+    for(std::size_t i = 0; i < var.bits.size(); i++)
     {
       if(var.is_latch())
       {
-        out << "ASSIGN next(" << id2smv(it->first);
+        out << "ASSIGN next(" << id2smv(var_it.first);
         if(var.bits.size() != 1)
           out << "[" << i << "]";
         out << "):=";
@@ -249,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
     {