Change sby task name from prove to bmc (we do bmc, not unbounded prove)

formal/Makefile

@@ -8,7 +8,7 @@ all: ${psl_tests}
 
 %: ../src/%.vhd ../src/pkg.vhd ../src/sequencer.vhd ../src/hex_sequencer.vhd %.sby
 	mkdir -p work
-	-sby --yosys "yosys -m ghdl" -f -d work/$@ $@.sby prove
+	-sby --yosys "yosys -m ghdl" -f -d work/$@ $@.sby bmc
 
 
 clean:

formal/psl_always.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_always.vhd -e psl_always
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_always.vhd -e psl_always
 prep -top psl_always
 
 [files]

formal/psl_before.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_before.vhd -e psl_before
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_before.vhd -e psl_before
 prep -top psl_before
 
 [files]

formal/psl_eventually.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_eventually.vhd -e psl_eventually
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_eventually.vhd -e psl_eventually
 prep -top psl_eventually
 
 [files]

formal/psl_logical_implication.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_logical_implication.vhd -e psl_logical_implication
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_logical_implication.vhd -e psl_logical_implication
 prep -top psl_logical_implication
 
 [files]

formal/psl_never.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_never.vhd -e psl_never
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_never.vhd -e psl_never
 prep -top psl_never
 
 [files]

formal/psl_next.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next.vhd -e psl_next
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_next.vhd -e psl_next
 prep -top psl_next
 
 [files]

formal/psl_next_3.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_3.vhd -e psl_next_3
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_3.vhd -e psl_next_3
 prep -top psl_next_3
 
 [files]

formal/psl_next_a.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_a.vhd -e psl_next_a
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_a.vhd -e psl_next_a
 prep -top psl_next_a
 
 [files]

formal/psl_next_e.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_e.vhd -e psl_next_e
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_e.vhd -e psl_next_e
 prep -top psl_next_e
 
 [files]

formal/psl_next_event.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_event.vhd -e psl_next_event
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_event.vhd -e psl_next_event
 prep -top psl_next_event
 
 [files]

formal/psl_next_event_4.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_event_4.vhd -e psl_next_event_4
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_event_4.vhd -e psl_next_event_4
 prep -top psl_next_event_4
 
 [files]

formal/psl_next_event_a.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd hex_sequencer.vhd psl_next_event_a.vhd -e psl_next_event_a
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd hex_sequencer.vhd psl_next_event_a.vhd -e psl_next_event_a
 prep -top psl_next_event_a
 
 [files]

formal/psl_next_event_e.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_event_e.vhd -e psl_next_event_e
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_event_e.vhd -e psl_next_event_e
 prep -top psl_next_event_e
 
 [files]

formal/psl_sere.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere.vhd -e psl_sere
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere.vhd -e psl_sere
 prep -top psl_sere
 
 [files]

formal/psl_sere_non_overlapping_suffix_impl.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere_non_overlapping_suffix_impl.vhd -e psl_sere_non_overlapping_suffix_impl
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere_non_overlapping_suffix_impl.vhd -e psl_sere_non_overlapping_suffix_impl
 prep -top psl_sere_non_overlapping_suffix_impl
 
 [files]

formal/psl_sere_overlapping_suffix_impl.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere_overlapping_suffix_impl.vhd -e psl_sere_overlapping_suffix_impl
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere_overlapping_suffix_impl.vhd -e psl_sere_overlapping_suffix_impl
 prep -top psl_sere_overlapping_suffix_impl
 
 [files]

formal/psl_until.sby

@@ -1,15 +1,15 @@
 [tasks]
-prove
+bmc
 
 [options]
 depth 25
-prove: mode bmc
+bmc: mode bmc
 
 [engines]
-prove: smtbmc z3
+bmc: smtbmc z3
 
 [script]
-prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_until.vhd -e psl_until
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_until.vhd -e psl_until
 prep -top psl_until
 
 [files]