Merge pull request #1096 from diffblue/bdd-sva-via-ltl

BDD engine: transform SVA to LTL, then LTL to CTL

Author: tautschnig

regression/verilog/SVA/followed-by1.bdd.desc

@@ -0,0 +1,10 @@
+CORE
+followed-by1.sv
+--bdd
+^\[main\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): PROVED$
+^\[main\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/followed-by1.desc renamed to regression/verilog/SVA/followed-by1.bmc.desc

@@ -0,0 +1,10 @@
+CORE
+followed-by2.sv
+--bdd
+^\[main\.p0\] always \(\(main\.a #-# main\.b\) iff \(not \(main\.a |-> \(not main\.b\)\)\)\): PROVED$
+^\[main\.p1\] always \(\(main\.a #=# main\.b\) iff \(not \(main\.a |=> \(not main\.b\)\)\)\): FAILURE: property not supported by BDD engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/followed-by2.bdd.desc

@@ -0,0 +1,11 @@
+CORE
+followed-by4.sv
+--bdd
+^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$
+^\[main\.p2\] \(1 or \(##2 1\)\) #-# main\.x == 2: FAILURE: property not supported by BDD engine$
+^\[main\.p3\] \(1 or \(##2 1\)\) #-# main\.x == 0: FAILURE: property not supported by BDD engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/followed-by2.desc renamed to regression/verilog/SVA/followed-by2.bmc.desc

@@ -0,0 +1,14 @@
+CORE
+initial1.sv
+--bdd
+^\[main\.p0\] main\.counter == 0: PROVED$
+^\[main\.p1\] main\.counter == 100: REFUTED$
+^\[main\.p2\] ##1 main\.counter == 1: PROVED$
+^\[main\.p3\] ##1 main\.counter == 100: REFUTED$
+^\[main\.p4\] s_nexttime main\.counter == 1: PROVED$
+^\[main\.p5\] always \[1:1\] main\.counter == 1: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/followed-by4.bdd.desc

@@ -0,0 +1,11 @@
+CORE
+nexttime1.sv
+--bdd
+^\[main\.p1\] s_nexttime\[0\] main\.counter == 0: PROVED$
+^\[main\.p2\] s_nexttime\[1\] main\.counter == 1: PROVED$
+^\[main\.p3\] nexttime\[8\] main\.counter == 8: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/followed-by4.desc renamed to regression/verilog/SVA/followed-by4.bmc.desc

@@ -0,0 +1,10 @@
+CORE
+restrict1.sv
+--bdd
+^\[main\.p0\] always main\.x != 5: ASSUMED$
+^\[main\.p1\] always main\.x != 6: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/initial1.bdd.desc

@@ -0,0 +1,8 @@
+CORE
+s_eventually1.sv
+--bdd
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/initial1.desc renamed to regression/verilog/SVA/initial1.bmc.desc

@@ -0,0 +1,8 @@
+CORE
+sequence4.sv
+--bdd
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/nexttime1.bdd.desc

@@ -0,0 +1,13 @@
+CORE
+sequence_and1.sv
+--bdd
+^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$
+^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$
+^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED$
+^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED$
+^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/nexttime1.desc renamed to regression/verilog/SVA/nexttime1.bmc.desc

@@ -1,13 +1,13 @@
 module main(input clk);
 
-  reg [31:0] x = 0;
+  reg [7:0] x = 0;
 
   // 0 1 2 3 4 ...
   always_ff @(posedge clk)
     x<=x+1;
 
   // 0 0 1 1 2 2 3 3 ...
-  wire [31:0] half_x = x/2;
+  wire [7:0] half_x = x/2;
 
   // should pass
   initial p0: assert property (half_x==0[*2]);

regression/verilog/SVA/restrict1.bdd.desc

@@ -1,13 +1,13 @@
 module main(input clk);
 
-  reg [31:0] x = 0;
+  reg [7:0] x = 0;
 
   // 0 1 2 3 4 ...
   always_ff @(posedge clk)
     x<=x+1;
 
   // 0 0 1 1 2 2 3 3 ...
-  wire [31:0] half_x = x/2;
+  wire [7:0] half_x = x/2;
 
   // should pass
   initial p0: assert property (x==0[*]);

regression/verilog/SVA/restrict1.desc renamed to regression/verilog/SVA/restrict1.bmc.desc

@@ -1,13 +1,13 @@
 module main(input clk);
 
-  reg [31:0] x = 0;
+  reg [7:0] x = 0;
 
   // 0 1 2 3 4 ...
   always_ff @(posedge clk)
     x<=x+1;
 
   // 0 0 1 1 2 2 3 3 ...
-  wire [31:0] half_x = x/2;
+  wire [7:0] half_x = x/2;
 
   // should pass
   initial p0: assert property (x==0[*1] #=# x==1[*1]);

regression/verilog/SVA/s_eventually1.bdd.desc

@@ -1,7 +1,6 @@
 CORE
 past1.sv
 --bdd
-^\[main\.p0\] ##0 \$past\(main\.counter, 0\) == 0: FAILURE: property not supported by BDD engine$
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/s_eventually1.desc renamed to regression/verilog/SVA/s_eventually1.bmc.desc

@@ -1,6 +1,6 @@
 module main(input clk);
 
-  reg [31:0] counter = 0;
+  reg [7:0] counter = 0;
 
   always @(posedge clk)
     counter++;

regression/verilog/SVA/sequence4.bdd.desc

@@ -23,7 +23,6 @@ Author: Daniel Kroening, [email protected]
 #include <trans-netlist/instantiate_netlist.h>
 #include <trans-netlist/trans_trace_netlist.h>
 #include <trans-netlist/unwind_netlist.h>
-#include <verilog/sva_expr.h>
 
 #include "netlist.h"
 
@@ -66,7 +65,7 @@ class bdd_enginet
   const namespacet ns;
   netlistt netlist;
 
-  static bool property_supported(const exprt &);
+  static std::optional<exprt> property_supported(const exprt &);
 
   // the Manager must appear before any BDDs
   // to do the cleanup in the right order
@@ -199,9 +198,20 @@ property_checker_resultt bdd_enginet::operator()()
                          << ", nodes: " << netlist.number_of_nodes()
                          << messaget::eom;
 
-    for(const auto &property : properties.properties)
-      if(property_supported(property.normalized_expr))
-        get_atomic_propositions(property.normalized_expr);
+    for(auto &property : properties.properties)
+    {
+      if(!property.is_disabled() && !property.is_assumed())
+      {
+        auto converted_opt = property_supported(property.normalized_expr);
+        if(converted_opt.has_value())
+        {
+          property.normalized_expr = *converted_opt;
+          get_atomic_propositions(*converted_opt);
+        }
+        else
+          property.failure("property not supported by BDD engine");
+      }
+    }
 
     message.status() << "Building BDD for netlist" << messaget::eom;
 
@@ -449,40 +459,29 @@ Function: bdd_enginet::property_supported
 
 \*******************************************************************/
 
-bool bdd_enginet::property_supported(const exprt &expr)
+std::optional<exprt> bdd_enginet::property_supported(const exprt &expr)
 {
   // Our engine knows all of CTL.
   if(is_CTL(expr))
-    return true;
+    return expr;
 
   if(is_LTL(expr))
   {
     // We can map selected path properties to CTL.
-    return LTL_to_CTL(expr).has_value();
+    return LTL_to_CTL(expr);
   }
 
   if(is_SVA(expr))
   {
-    if(
-      expr.id() == ID_sva_always &&
-      !has_temporal_operator(to_sva_always_expr(expr).op()))
-    {
-      // always p
-      return true;
-    }
-
-    if(
-      expr.id() == ID_sva_always &&
-      to_sva_always_expr(expr).op().id() == ID_sva_s_eventually &&
-      !has_temporal_operator(
-        to_sva_s_eventually_expr(to_sva_always_expr(expr).op()).op()))
-    {
-      // always s_eventually p
-      return true;
-    }
+    // We can map some SVA to LTL. In turn, some of that can be mapped to CTL.
+    auto ltl_opt = SVA_to_LTL(expr);
+    if(ltl_opt.has_value())
+      return property_supported(ltl_opt.value());
+    else
+      return {};
   }
 
-  return false;
+  return {};
 }
 
 /*******************************************************************\
@@ -505,51 +504,12 @@ void bdd_enginet::check_property(propertyt &property)
   if(property.is_assumed())
     return;
 
-  if(!property_supported(property.normalized_expr))
-  {
-    property.failure("property not supported by BDD engine");
+  if(property.is_failure())
     return;
-  }
 
   message.status() << "Checking " << property.name << messaget::eom;
   property.status=propertyt::statust::UNKNOWN;
 
-  if(
-    property.normalized_expr.id() == ID_sva_always &&
-    to_sva_always_expr(property.normalized_expr).op().id() ==
-      ID_sva_s_eventually &&
-    !has_temporal_operator(to_sva_s_eventually_expr(
-                             to_sva_always_expr(property.normalized_expr).op())
-                             .op()))
-  {
-    // always s_eventually p --> AG AF p
-    auto p = to_sva_s_eventually_expr(
-               to_sva_always_expr(property.normalized_expr).op())
-               .op();
-    property.normalized_expr = AG_exprt{AF_exprt{p}};
-  }
-
-  if(
-    property.normalized_expr.id() == ID_sva_always &&
-    !has_temporal_operator(to_sva_always_expr(property.normalized_expr).op()))
-  {
-    // always p --> AG p
-    auto p = to_sva_always_expr(property.normalized_expr).op();
-    property.normalized_expr = AG_exprt{p};
-  }
-
-  // Our engine knows CTL only.
-  // We map selected path properties to CTL.
-  if(
-    has_temporal_operator(property.normalized_expr) &&
-    is_LTL(property.normalized_expr))
-  {
-    auto CTL_opt = LTL_to_CTL(property.normalized_expr);
-    CHECK_RETURN(CTL_opt.has_value());
-    property.normalized_expr = CTL_opt.value();
-    CHECK_RETURN(is_CTL(property.normalized_expr));
-  }
-
   if(is_AGp(property.normalized_expr))
   {
     check_AGp(property);