Test combination of k-induction and Buechi instrumentation

regression/ebmc-spot/sva-buechi/cycle_delay2.k.desc

@@ -0,0 +1,7 @@
+CORE
+../../verilog/SVA/cycle_delay2.sv
+--buechi --k-induction --bound 3
+^\[.*\] ##\[1:2\] main\.x == 2: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc-spot/sva-buechi/empty_sequence1.k.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/empty_sequence1.sv
+--buechi --k-induction --bound 1
+^\[main\.p0\] 1 \[\*0\]: REFUTED$
+^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED$
+^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED$
+^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$
+^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/eventually1.k.desc

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/eventually1.sv
+--buechi --k-induction --bound 2
+^\[main\.p0\] always \(main\.counter == 1 implies \(eventually \[1:2\] main\.counter == 3\)\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc-spot/sva-buechi/eventually4.k.desc

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/eventually4.sv
+--buechi --k-induction --bound 1
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/followed-by1.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/followed-by1.sv
+--buechi --k-induction --bound 1
+^\[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/ebmc-spot/sva-buechi/followed-by2.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/followed-by2.sv
+--buechi --k-induction --bound 1
+^\[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\)\)\)\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/followed-by4.k.desc

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/followed-by4.sv
+--buechi --k-induction --bound 3
+^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$
+^\[main\.p2\] \(1 or \(##2 1\)\) #-# main\.x == 2: PROVED$
+^\[main\.p3\] \(1 or \(##2 1\)\) #-# main\.x == 0: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/if1.sv
+--buechi --k-induction --bound 1
+^\[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/immediate1.k.desc

@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/immediate1.sv
+--buechi --k-induction --bound 1
+^\[main\.assert\.1\] always main\.x & 1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/initial1.k.desc

@@ -0,0 +1,14 @@
+CORE
+../../verilog/SVA/initial1.sv
+--buechi --k-induction --bound 2
+^\[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/ebmc-spot/sva-buechi/initial2.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/initial2.sv
+--buechi --k-induction --bound 1 --module main
+^\[main\.assert\.1\] main\.counter == 1: PROVED$
+^\[main\.assert\.2\] main\.counter == 2: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

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

regression/ebmc-spot/sva-buechi/nexttime1.k.desc

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/nexttime1.sv
+--buechi --k-induction --bound 9
+^\[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/ebmc-spot/sva-buechi/restrict1.k.desc

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

regression/ebmc-spot/sva-buechi/s_always1.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/s_always1.sv
+--buechi --k-induction --bound 10
+^\[main\.p0\] s_always \[0:9\] main\.x < 10: PROVED$
+^\[main\.p1\] not \(s_always \[0:9\] main\.x < 10\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/s_eventually2.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/s_eventually2.sv
+--buechi --k-induction --bound 2
+^\[main\.p0\] always s_eventually main.reset \|\| main\.counter == 10: UNSUPPORTED: unsupported by k-induction$
+^\[main\.p1\] always \(s_eventually \[0:2\] main.reset \|\| main\.counter == 10\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence2.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence2.sv
+--buechi --k-induction --bound 1
+^\[main\.p0] weak\(##\[0:\$\] main\.x == 10\): PROVED$
+^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: unsupported by k-induction$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence4.k.desc

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/sequence4.sv
+--buechi --k-induction --bound 1
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence6.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence6.sv
+--buechi --k-induction --bound 2
+^\[main\.p0\] \(1 ##1 1\) \|-> main\.x == 1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+

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

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

regression/ebmc-spot/sva-buechi/sequence_and3.k.desc

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/sequence_and3.sv
+--buechi --k-induction --bound 3
+^\[.*\] \(\(1 or \(##2 1\)\) and 1\) \|-> main\.x == 2: REFUTED$
+^\[.*\] \(1 and \(1 or \(##2 1\)\)\) \|-> main\.x == 2: REFUTED$
+^\[.*\] \(\(1 or \(##2 1\)\) and 1\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED$
+^\[.*\] \(1 and \(1 or \(##2 1\)\)\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_implication1.k.desc

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/sequence_implication1.sv
+--buechi --k-induction --bound 2
+^\[.*\] always \(\(main\.counter == 1 ##1 main\.counter == 2\) \|-> \(##1 main.counter == 0\)\): PROVED$
+^\[.*\] always \(\(main\.counter == 1 ##1 main\.counter == 2\) \|=> main\.counter == 0\): PROVED$
+^\[.*\] always \(0 \|-> 0\): PROVED$
+^\[.*\] \(1 or \(##1 1\)\) \|-> main\.counter == 0: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_intersect1.k.desc

@@ -0,0 +1,14 @@
+CORE
+../../verilog/SVA/sequence_intersect1.sv
+--buechi --k-induction --bound 4
+^\[main\.p0\] main\.x == 0 intersect main\.x == 1: REFUTED$
+^\[main\.p1\] always main\.x >= 0: PROVED$
+^\[main\.p2\] always main\.x <= 5: PROVED$
+^\[main\.p3\] always main\.x <= 3: REFUTED$
+^\[main\.p4\] always \(main\.x >= 0 intersect main\.x <= 5\): PROVED$
+^\[main\.p5\] always \(main\.x >= 0 intersect main\.x <= 3\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_or1.k.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sequence_or1.sv
+--buechi --k-induction --bound 2
+^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED$
+^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED$
+^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED$
+^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED$
+^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_repetition1.k.desc

@@ -0,0 +1,14 @@
+CORE
+../../verilog/SVA/sequence_repetition1.sv
+--buechi --k-induction --bound 2
+^\[.*\] main\.half_x == 0 \[\*2\]: PROVED$
+^\[.*\] main\.half_x == 0 \[->2\]: UNSUPPORTED: unsupported by k-induction$
+^\[.*\] main\.half_x == 0 \[=2\]: UNSUPPORTED: unsupported by k-induction$
+^\[.*\] main\.x == 0 \[\*2\]: REFUTED$
+^\[.*\] main\.x == 0 \[->2\]: UNSUPPORTED: unsupported by k-induction$
+^\[.*\] main\.x == 0 \[=2\]: UNSUPPORTED: unsupported by k-induction$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/sequence_repetition3.sv
+--buechi --k-induction --bound 2
+^\[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/sequence_repetition4.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_repetition4.sv
+--buechi --k-induction --bound 4
+^\[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_repetition5.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_repetition5.sv
+--buechi --k-induction --bound 10
+^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:9\]\) ##1 main.pulse: PROVED$
+^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:8\]\) ##1 main.pulse: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_repetition7.sv
+--buechi --k-induction --bound 2
+^\[.*\] \(main\.a ##1 main\.b\) \[\*5\]: PROVED$
+^\[.*\] \(\!main\.b ##1 \!main\.a\) \[\*5\]: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/stable1.k.desc

@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/stable1.sv
+--buechi --k-induction --bound 2
+^\[main\.p0\] always \(\$stable\(main\.data\) \|=> main\.counter >= 1\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/static_final1.k.desc

@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/static_final1.sv
+--buechi --k-induction --bound 1
+^\[full_adder\.p0\] 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/sva_abort1.k.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sva_abort1.sv
+--buechi --k-induction --bound 2
+^\[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
+--

regression/ebmc-spot/sva-buechi/sva_iff2.k.desc

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/sva_iff2.sv
+--buechi --k-induction --bound 1
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sva_implies2.k.desc

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/sva_implies2.sv
+--buechi --k-induction --bound 2
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--