Merge pull request #1363 from diffblue/sva-buechi-tests

additional tests for SVA->Buechi

Author: tautschnig

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

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/immediate2.sv
+--buechi
+^\[main\.assume\.1\] assume always 0: ASSUMED$
+^\[main\.assert\.2\] always main\.index < 10: PROVED \(.*\)$
+^\[main\.assert\.3\] always 0: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/immediate3.sv
+--buechi
+^\[full_adder\.assert\.1\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED \(.*\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/s_eventually4.sv
+--buechi --module main --bound 11
+^\[main\.p0\] always \(\(s_eventually main\.counter == 1\) or \(s_eventually main.counter == 10\)\): PROVED up to bound 11$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/sequence3.sv
+--buechi --bound 20 --numbered-trace
+^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,17 @@
+CORE
+../../verilog/SVA/sequence_repetition2.sv
+--buechi --bound 10
+^\[main\.p0\] main\.x == 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p1\] \(main\.x == 0 \[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
+^\[main\.p2\] main\.x == 0 \[\+\]: PROVED up to bound 10$
+^\[main\.p3\] main\.half_x == 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p4\] main\.x == 1 \[\*\]: REFUTED$
+^\[main\.p5\] 0 \[\*\]: REFUTED$
+^\[main\.p6\] main\.x == 1 \[\+\]: REFUTED$
+^\[main\.p7\] \(main\.x == 0 \[\+\]\) #-# main\.x == 1: REFUTED$
+^\[main\.p8\] 0 \[\+\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

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

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

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/system_verilog_assertion1.sv
+--buechi --module main --bound 20 --trace
+^EXIT=10$
+^SIGNAL=0$
+^Counterexample:$
+--
+^warning: ignoring

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

@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/system_verilog_assertion2.sv
+--buechi --module main --bound 20 --trace
+^EXIT=10$
+^SIGNAL=0$
+^Counterexample:$
+^\[main\.my_label\] .* REFUTED$
+--
+^warning: ignoring

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

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/system_verilog_assertion4.sv
+--buechi --module main --bound 10
+^\[main\.p11\] always \(main\.x == 0 \|-> \(\(##1 main\.x == 1\) and \(not \(##2 main\.x == 3\)\)\)\): UNSUPPORTED: not convertible to Buechi$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

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

@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/weak1.sv
+--buechi --bound 20
+^\[main\.p0\] weak\(##\[0:9\] main\.x == 100\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--