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

The BDD engine now transforms SVA to LTL, when possible, which in turn is
transformed to CTL, when possible.

This is strictly more general than the current direct mapping.

Author: kroening

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);