Merge pull request #449 from diffblue/netlist-bmc-unsupported-property

netlist-BMC now gives error for unsupported properties

Author: tautschnig

regression/ebmc/smv/bmc_unsupported_property3.desc

@@ -0,0 +1,9 @@
+CORE
+bmc_unsupported_property3.smv
+--aig
+^EXIT=10$
+^SIGNAL=0$
+^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by netlist BMC engine$
+^\[main::spec2\] G main::var::x = FALSE: REFUTED$
+--
+^warning: ignoring

regression/ebmc/smv/bmc_unsupported_property3.smv

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

src/ebmc/ebmc_base.cpp

@@ -77,6 +77,9 @@ int ebmc_baset::finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver)
     if(property.is_disabled())
       continue;
 
+    if(property.is_failure())
+      continue;
+
     message.status() << "Checking " << property.name << messaget::eom;
 
     literalt property_literal=!solver.land(property.timeframe_literals);
@@ -199,6 +202,12 @@ int ebmc_baset::do_bit_level_bmc(cnft &solver, bool convert_only)
       if(property.is_disabled())
         continue;
 
+      if(!netlist_bmc_supports_property(property.normalized_expr))
+      {
+        property.failure("property not supported by netlist BMC engine");
+        continue;
+      }
+
       ::unwind_property(
         property.normalized_expr,
         property.timeframe_literals,

src/trans-netlist/unwind_netlist.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/ebmc_util.h>
 
 #include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
 #include "instantiate_netlist.h"
@@ -199,3 +200,27 @@ void unwind_property(
   }
 }
 
+/*******************************************************************\
+
+Function: netlist_bmc_supports_property
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool netlist_bmc_supports_property(const exprt &expr)
+{
+  // We do AG p only.
+  if(expr.id() == ID_AG)
+    return !has_temporal_operator(to_AG_expr(expr).op());
+  else if(expr.id() == ID_G)
+    return !has_temporal_operator(to_G_expr(expr).op());
+  else if(expr.id() == ID_sva_always)
+    return !has_temporal_operator(to_sva_always_expr(expr).op());
+  else
+    return false;
+}

src/trans-netlist/unwind_netlist.h

@@ -42,6 +42,9 @@ void unwind_property(
   const bmc_mapt &,
   const namespacet &);
 
+// Is the property supported?
+bool netlist_bmc_supports_property(const exprt &);
+
 // unwind a property that is given as netlist node
 void unwind_property(
   const bmc_mapt &,