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
+--