additional tests for the SVA->Buechi flow

Author: kroening

regression/ebmc-spot/sva-buechi/disable_iff1.bdd.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+../../verilog/SVA/disable_iff1.sv
+--buechi --module main --bdd --numbered-trace
+^\[main\.p0\] always \(disable iff \(main.counter == 0\) main\.counter != 0\): PROVED$
+^\[main\.p1\] always \(disable iff \(1\) 0\): PROVED$
+^\[main\.p2\] always \(disable iff \(main\.counter == 1\) main\.counter == 0\): REFUTED$
+^Counterexample with 3 states:$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The trace is missing.

regression/ebmc-spot/sva-buechi/if1.bdd.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/if1.sv
+--buechi --bdd
+^\[main\.p0\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1\): PROVED$
+^\[main\.p1\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/issue669.desc

@@ -0,0 +1,17 @@
+CORE
+../../verilog/SVA/issue669.sv
+--buechi --bound 5 --top top
+\[top\.assert\.1\] always not s_eventually 0: PROVED up to bound 5$
+\[top\.assert\.2\] always \(\(top\.a until_with top\.b\) implies \(not \(\(not top\.b\) s_until \(not top\.a\)\)\)\): PROVED up to bound 5$
+\[top\.assert\.3\] always \(\(not \(\(not top\.b\) s_until \(not top\.a\)\)\) implies \(top\.a until_with top\.b\)\): PROVED up to bound 5$
+\[top\.assert\.4\] always \(\(top\.a until_with top\.b\) implies \(top\.a until \(top\.a and top\.b\)\)\): PROVED up to bound 5$
+\[top\.assert\.5\] always \(\(top\.a until \(top\.a and top\.b\)\) implies \(top\.a until_with top\.b\)\): PROVED up to bound 5$
+\[top\.assert\.6\] always \(\(s_eventually top\.a\) implies \(1 s_until top\.a\)\): PROVED up to bound 5$
+\[top\.assert\.7\] always \(\(1 s_until top\.a\) implies \(s_eventually top\.a\)\): PROVED up to bound 5$
+\[top\.assert\.8\] always \(\(top\.a s_until top\.b\) implies \(\(s_eventually top\.b\) and \(top\.a until top\.b\)\)\): PROVED up to bound 5$
+\[top\.assert\.9\] always \(\(\(s_eventually top\.b\) and \(top\.a until top\.b\)\) implies \(top\.a s_until top\.b\)\): PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+https://github.com/diffblue/hw-cbmc/issues/669

regression/ebmc-spot/sva-buechi/sequence_and2.bmc.desc

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/sequence_and2.sv
+--buechi
+\[.*\] \(1 and \(##2 1\)\) \|-> main\.x == 2: PROVED up to bound 5$
+\[.*\] \(\(##2 1\) and 1\) \|-> main\.x == 2: PROVED up to bound 5$
+\[.*\] \(\(##2 1\) and 1\) #-# main\.x == 2: PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_repetition4.bdd.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_repetition4.sv
+--buechi --bdd
+^\[main\.p0\] \(main\.x == 0 ##1 main\.x == 1\) \[\*2\]: PROVED$
+^\[main\.p1\] \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 0\) \[\*2\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_repetition7.bdd.desc

@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/sequence_repetition7.sv
+--buechi --bdd
+^\[.*\] \(main\.a ##1 main\.b\) \[\*5\]: PROVED$
+^\[.*\] \(\!main\.b ##1 \!main\.a\) \[\*5\]: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/ebmc-spot/sva-buechi/sva_abort1.bdd.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sva_abort1.sv
+--buechi --module main --bdd
+^\[main\.p0\] always \(accept_on \(main\.counter == 0\) main\.counter != 0\): PROVED$
+^\[main\.p1\] always \(accept_on \(1\) 0\): PROVED$
+^\[main\.p2\] always \(accept_on \(main\.counter == 1\) main\.counter == 0\): REFUTED$
+^\[main\.p3\] always \(reject_on \(main\.counter != 0\) 1\): REFUTED$
+^\[main\.p4\] always \(reject_on \(1\) 1\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--