Implement SVA cover in BMC

This adds support for SVA cover properties to the BMC engine.
diffblue · Apr 15, 2024 · c89476e · c89476e
1 parent 5612fe0
commit c89476e
Show file tree

Hide file tree

Showing 9 changed files with 87 additions and 39 deletions.
diff --git a/regression/verilog/SVA/cover1.desc b/regression/verilog/SVA/cover1.desc
@@ -1,8 +1,11 @@
-KNOWNBUG
+CORE
 cover1.sv
---bound 10
-^\[main\.property\.p0\] cover main\.counter == 1: REFUTED$
-^\[main\.property\.p1\] cover main\.counter == 100: REFUTED$
+--bound 10 --numbered-trace
+^\[main\.property\.p0\] cover main\.counter == 1: PROVED$
+^Trace:$
+^main\.counter@0 = 0$
+^main\.counter@1 = 1$
+^\[main\.property\.p1\] cover main\.counter == 100: REFUTED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --

diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp
@@ -402,7 +402,7 @@ void bdd_enginet::compute_counterexample(
     throw "unexpected result from SAT solver";
   }
 
-  property.counterexample =
+  property.witness_trace =
     compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);
 }
 

diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp
@@ -98,17 +98,25 @@ void bmc(
 
       message.status() << "Checking " << property.name << messaget::eom;
 
-      auto assumption = not_exprt(conjunction(property.timeframe_handles));
+      auto assumption = not_exprt{conjunction(property.timeframe_handles)};
 
       decision_proceduret::resultt dec_result = solver(assumption);
 
       switch(dec_result)
       {
       case decision_proceduret::resultt::D_SATISFIABLE:
-        property.refuted();
-        message.result() << "SAT: counterexample found" << messaget::eom;
-
-        property.counterexample = compute_trans_trace(
+        if(property.is_exists_path())
+        {
+          property.proved();
+          message.result() << "SAT: path found" << messaget::eom;
+        }
+        else // universal path property
+        {
+          property.refuted();
+          message.result() << "SAT: counterexample found" << messaget::eom;
+        }
+
+        property.witness_trace = compute_trans_trace(
           property.timeframe_handles,
           solver,
           bound + 1,
@@ -117,9 +125,18 @@ void bmc(
         break;
 
       case decision_proceduret::resultt::D_UNSATISFIABLE:
-        message.result() << "UNSAT: No counterexample found within bound"
-                         << messaget::eom;
-        property.proved_with_bound(bound);
+        if(property.is_exists_path())
+        {
+          message.result() << "UNSAT: No path found within bound"
+                           << messaget::eom;
+          property.refuted_with_bound(bound);
+        }
+        else // universal path property
+        {
+          message.result() << "UNSAT: No counterexample found within bound"
+                           << messaget::eom;
+          property.proved_with_bound(bound);
+        }
         break;
 
       case decision_proceduret::resultt::D_ERROR:

diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp
@@ -95,7 +95,7 @@ int ebmc_baset::finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver)
 
         namespacet ns(transition_system.symbol_table);
 
-        property.counterexample =
+        property.witness_trace =
           compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);
       }
       break;

diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp
@@ -26,6 +26,8 @@ std::string ebmc_propertiest::propertyt::status_as_string() const
     return "PROVED up to bound " + std::to_string(bound);
   case statust::REFUTED:
     return "REFUTED";
+  case statust::REFUTED_WITH_BOUND:
+    return "REFUTED up to bound " + std::to_string(bound);
   case statust::UNKNOWN:
     return "UNKNOWN";
   case statust::INCONCLUSIVE:

diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 
 #include <solvers/prop/literal.h>
+#include <temporal-logic/temporal_logic.h>
 #include <trans-netlist/trans_trace.h>
 #include <trans-word-level/property.h>
 
@@ -37,23 +38,24 @@ class ebmc_propertiest
 
     enum class statust
     {
-      UNKNOWN,           // no work done yet
-      DISABLED,          // turned off by user
-      PROVED,            // property is true, unbounded
-      PROVED_WITH_BOUND, // property is true, with bound
-      REFUTED,           // property is false, possibly counterexample
-      DROPPED,           // given up
-      FAILURE,           // error during anaysis
-      INCONCLUSIVE       // analysis can't determine truth
+      UNKNOWN,            // no work done yet
+      DISABLED,           // turned off by user
+      PROVED,             // property is true, unbounded
+      PROVED_WITH_BOUND,  // property is true, with bound
+      REFUTED,            // property is false, possibly counterexample
+      REFUTED_WITH_BOUND, // property is false, with bound
+      DROPPED,            // given up
+      FAILURE,            // error during anaysis
+      INCONCLUSIVE        // analysis can't determine truth
     } status = statust::UNKNOWN;
 
     std::size_t bound = 0;
-    std::optional<trans_tracet> counterexample;
+    std::optional<trans_tracet> witness_trace;
     std::optional<std::string> failure_reason;
 
-    bool has_counterexample() const
+    bool has_witness_trace() const
     {
-      return counterexample.has_value();
+      return witness_trace.has_value();
     }
 
     bool is_unknown() const
@@ -122,6 +124,12 @@ class ebmc_propertiest
       status = statust::REFUTED;
     }
 
+    void refuted_with_bound(std::size_t _bound)
+    {
+      status = statust::REFUTED_WITH_BOUND;
+      bound = _bound;
+    }
+
     void drop()
     {
       status = statust::DROPPED;
@@ -146,6 +154,11 @@ class ebmc_propertiest
     {
       return ::requires_lasso_constraints(normalized_expr);
     }
+
+    bool is_exists_path() const
+    {
+      return ::is_exists_path(original_expr);
+    }
   };
 
   typedef std::list<propertyt> propertiest;

diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp
@@ -58,9 +58,8 @@ void report_results(
       json_property["identifier"] = json_stringt(id2string(property.name));
       json_property["status"] = json_stringt(property.status_as_string());
 
-      if(property.has_counterexample())
-        json_property["counterexample"] =
-          json(property.counterexample.value(), ns);
+      if(property.has_witness_trace())
+        json_property["trace"] = json(property.witness_trace.value(), ns);
 
       json_properties.push_back(std::move(json_property));
     }
@@ -81,8 +80,8 @@ void report_results(
       xml_result.set_attribute("property", id2string(property.name));
       xml_result.set_attribute("status", property.status_as_string());
 
-      if(property.has_counterexample())
-        xml_result.new_element() = xml(property.counterexample.value(), ns);
+      if(property.has_witness_trace())
+        xml_result.new_element() = xml(property.witness_trace.value(), ns);
 
       std::cout << xml_result << '\n' << std::flush;
     }
@@ -109,6 +108,7 @@ void report_results(
       case statust::PROVED: message.status() << messaget::green; break;
       case statust::PROVED_WITH_BOUND: message.status() << messaget::green; break;
       case statust::REFUTED: message.status() << messaget::bright_red; break;
+      case statust::REFUTED_WITH_BOUND: message.status() << messaget::bright_red; break;
       case statust::DROPPED: message.status() << messaget::red; break;
       case statust::FAILURE: message.status() << messaget::red; break;
       case statust::UNKNOWN: message.status() << messaget::yellow; break;
@@ -121,24 +121,28 @@ void report_results(
 
       message.status() << messaget::reset << messaget::eom;
 
-      if(property.has_counterexample())
+      if(property.has_witness_trace())
       {
+        auto term = [&property]() {
+          return property.is_exists_path() ? "Trace" : "Counterexample";
+        };
+
         if(cmdline.isset("trace"))
         {
-          message.status() << "Counterexample:\n" << messaget::eom;
+          message.status() << term() << ":\n" << messaget::eom;
           show_trans_trace(
-            property.counterexample.value(), message, ns, std::cout);
+            property.witness_trace.value(), message, ns, std::cout);
         }
         else if(cmdline.isset("numbered-trace"))
         {
-          message.status() << "Counterexample:\n" << messaget::eom;
+          message.status() << term() << ":" << messaget::eom;
           show_trans_trace_numbered(
-            property.counterexample.value(), message, ns, std::cout);
+            property.witness_trace.value(), message, ns, std::cout);
         }
         else if(cmdline.isset("waveform"))
         {
-          message.status() << "Counterexample:" << messaget::eom;
-          show_waveform(property.counterexample.value(), ns);
+          message.status() << term() << ":" << messaget::eom;
+          show_waveform(property.witness_trace.value(), ns);
         }
       }
     }
@@ -148,13 +152,13 @@ void report_results(
   {
     for(const auto &property : properties.properties)
     {
-      if(property.has_counterexample())
+      if(property.has_witness_trace())
       {
         std::string vcdfile = cmdline.get_value("vcd");
         std::ofstream vcd(widen_if_needed(vcdfile));
 
         messaget message(message_handler);
-        show_trans_trace_vcd(property.counterexample.value(), message, ns, vcd);
+        show_trans_trace_vcd(property.witness_trace.value(), message, ns, vcd);
 
         break;
       }

diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
@@ -36,3 +36,8 @@ bool has_temporal_operator(const exprt &expr)
 
   return false;
 }
+
+bool is_exists_path(const exprt &expr)
+{
+  return expr.id() == ID_sva_cover;
+}
diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h
@@ -18,4 +18,8 @@ bool has_temporal_operator(const exprt &);
 /// as its root
 bool is_temporal_operator(const exprt &);
 
+/// Returns true iff the given expression is an existential path
+/// property.
+bool is_exists_path(const exprt &);
+
 #endif