Merge pull request #461 from diffblue/netlist-properties

SMV netlist output now includes temporal logic properties

Author: tautschnig

regression/ebmc/BDD/BDD_SVA1.desc

@@ -6,7 +6,7 @@ BDD_SVA1.sv
 ^\[top\.property\.p0\] always top\.my_bit: PROVED$
 ^\[top\.property\.p1\] always top\.my_bit: PROVED$
 ^\[top\.property\.p2\] always \(top\.counter == 3 \|-> \(nexttime top\.counter == 4\)\): FAILURE: property not supported by BDD engine$
-^\[top\.property\.p3\] always \(top\.counter == 3 \|=> top\.counter == 4\): PROVED$
+^\[top\.property\.p3\] always \(top\.counter == 3 \|=> top\.counter == 4\): FAILURE: property not supported by BDD engine$
 ^\[top\.property\.p4\] always \(top\.counter == 3 \|=> \(nexttime top\.counter == 5\)\): FAILURE: property not supported by BDD engine$
 ^\[top\.property\.p5\] always s_eventually top\.counter == 8: PROVED$
 ^\[top\.property\.p6\] always \(top\.counter == 0 \|-> \(s_eventually top\.counter == 8\)\): FAILURE: property not supported by BDD engine$

src/temporal-logic/temporal_logic.cpp

@@ -19,6 +19,7 @@ bool is_temporal_operator(const exprt &expr)
          expr.id() == ID_X || expr.id() == ID_sva_always ||
          expr.id() == ID_sva_always || expr.id() == ID_sva_ranged_always ||
          expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime ||
+         expr.id() == ID_sva_non_overlapped_implication ||
          expr.id() == ID_sva_until || expr.id() == ID_sva_s_until ||
          expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with ||
          expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually ||

src/trans-netlist/netlist.cpp

@@ -313,22 +313,50 @@ void netlistt::output_smv(std::ostream &out) const
   out << "-- Initial state" << '\n';
   out << '\n';
 
-  for(unsigned i=0; i<initial.size(); i++)
+  for(auto &initial_l : initial)
   {
-    out << "INIT ";
-    print_smv(out, initial[i]);
-    out << '\n';
+    if(!initial_l.is_true())
+    {
+      out << "INIT ";
+      print_smv(out, initial_l);
+      out << '\n';
+    }
   }
 
   out << '\n';
   out << "-- TRANS" << '\n';
   out << '\n';
 
-  for(unsigned i=0; i<transition.size(); i++)
+  for(auto &trans_l : transition)
   {
-    out << "TRANS ";
-    print_smv(out, transition[i]);
-    out << '\n';
+    if(!trans_l.is_true())
+    {
+      out << "TRANS ";
+      print_smv(out, trans_l);
+      out << '\n';
+    }
+  }
+
+  out << '\n';
+  out << "-- Properties" << '\n';
+  out << '\n';
+
+  for(auto &[id, property] : properties)
+  {
+    if(std::holds_alternative<Gpt>(property))
+    {
+      out << "-- " << id << '\n';
+      out << "LTLSPEC G ";
+      print_smv(out, std::get<Gpt>(property).p);
+      out << '\n';
+    }
+    else if(std::holds_alternative<GFpt>(property))
+    {
+      out << "-- " << id << '\n';
+      out << "LTLSPEC G F ";
+      print_smv(out, std::get<GFpt>(property).p);
+      out << '\n';
+    }
   }
 }
 

src/trans-netlist/netlist.h

@@ -9,11 +9,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_TRANS_NETLIST_H
 #define CPROVER_TRANS_NETLIST_H
 
-#include <iosfwd>
-
 #include "aig.h"
 #include "var_map.h"
 
+#include <iosfwd>
+#include <variant>
+
 class netlistt:public aig_plus_constraintst
 {
 public:
@@ -51,7 +52,23 @@ class netlistt:public aig_plus_constraintst
   // these are implicit conjunctions
   bvt initial;
   bvt transition;
-  
+
+  struct Gpt
+  {
+    literalt p;
+  };
+
+  struct GFpt
+  {
+    literalt p;
+  };
+
+  using propertyt = std::variant<Gpt, GFpt>;
+
+  // map from property ID to property netlist nodes
+  using propertiest = std::map<irep_idt, propertyt>;
+  propertiest properties;
+
 protected:
   static std::string id2smv(const irep_idt &id);
   void print_smv(std::ostream &out, literalt l) const;

src/trans-netlist/trans_to_netlist.cpp

@@ -6,18 +6,23 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include "trans_to_netlist.h"
+
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/ebmc_util.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 
 #include <solvers/flattening/boolbv_width.h>
+#include <temporal-logic/normalize_property.h>
+#include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/temporal_logic.h>
+#include <verilog/sva_expr.h>
 
 #include "aig_prop.h"
-#include "netlist.h"
-#include "trans_to_netlist.h"
 #include "instantiate_netlist.h"
+#include "netlist.h"
 
 /*******************************************************************\
 
@@ -303,6 +308,62 @@ void convert_trans_to_netlistt::operator()(const irep_idt &module)
   dest.initial.push_back(instantiate_convert(
     aig_prop, dest.var_map, trans.init(), ns, get_message_handler()));
 
+  // properties
+  for(const auto &[id, symbol] : symbol_table)
+  {
+    if(symbol.module == module && symbol.is_property)
+    {
+      auto expr = normalize_property(symbol.value);
+
+      auto convert = [&aig_prop, this](const exprt &expr) -> literalt {
+        return instantiate_convert(
+          aig_prop, dest.var_map, expr, ns, get_message_handler());
+      };
+
+      if(expr.id() == ID_AG || expr.id() == ID_G || expr.id() == ID_sva_always)
+      {
+        auto get_phi = [](const exprt &expr) {
+          if(expr.id() == ID_AG)
+            return to_AG_expr(expr).op();
+          else if(expr.id() == ID_G)
+            return to_G_expr(expr).op();
+          else if(expr.id() == ID_sva_always)
+            return to_sva_always_expr(expr).op();
+          else
+            PRECONDITION(false);
+        };
+
+        auto phi = get_phi(expr);
+
+        if(!has_temporal_operator(phi))
+        {
+          dest.properties.emplace(id, netlistt::Gpt{convert(phi)});
+        }
+        else if(
+          phi.id() == ID_AF || phi.id() == ID_F ||
+          phi.id() == ID_sva_s_eventually)
+        {
+          auto get_psi = [](const exprt &expr) {
+            if(expr.id() == ID_AF)
+              return to_AF_expr(expr).op();
+            else if(expr.id() == ID_F)
+              return to_F_expr(expr).op();
+            else if(expr.id() == ID_sva_s_eventually)
+              return to_sva_s_eventually_expr(expr).op();
+            else
+              PRECONDITION(false);
+          };
+
+          dest.properties.emplace(id, netlistt::GFpt{convert(get_psi(phi))});
+        }
+        else
+        {
+          // unsupported
+        }
+      }
+    }
+  }
+
   // find the nondet nodes
   for(std::size_t n=0; n<dest.nodes.size(); n++)
   {