From 78013a2d4e4bcc066a13db4a1fbb62ed5db445b1 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Thu, 14 May 2020 20:44:52 +0200 Subject: [PATCH] Change sby task name from prove to bmc (we do bmc, not unbounded prove) --- formal/Makefile | 2 +- formal/psl_always.sby | 8 ++++---- formal/psl_before.sby | 8 ++++---- formal/psl_eventually.sby | 8 ++++---- formal/psl_logical_implication.sby | 8 ++++---- formal/psl_never.sby | 8 ++++---- formal/psl_next.sby | 8 ++++---- formal/psl_next_3.sby | 8 ++++---- formal/psl_next_a.sby | 8 ++++---- formal/psl_next_e.sby | 8 ++++---- formal/psl_next_event.sby | 8 ++++---- formal/psl_next_event_4.sby | 8 ++++---- formal/psl_next_event_a.sby | 8 ++++---- formal/psl_next_event_e.sby | 8 ++++---- formal/psl_sere.sby | 8 ++++---- formal/psl_sere_non_overlapping_suffix_impl.sby | 8 ++++---- formal/psl_sere_overlapping_suffix_impl.sby | 8 ++++---- formal/psl_until.sby | 8 ++++---- 18 files changed, 69 insertions(+), 69 deletions(-) diff --git a/formal/Makefile b/formal/Makefile index d3ac780..8d16c94 100644 --- a/formal/Makefile +++ b/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: diff --git a/formal/psl_always.sby b/formal/psl_always.sby index c2f063a..ad4a556 100644 --- a/formal/psl_always.sby +++ b/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] diff --git a/formal/psl_before.sby b/formal/psl_before.sby index c95d7c7..191fc21 100644 --- a/formal/psl_before.sby +++ b/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] diff --git a/formal/psl_eventually.sby b/formal/psl_eventually.sby index 2aa85e7..9978be8 100644 --- a/formal/psl_eventually.sby +++ b/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] diff --git a/formal/psl_logical_implication.sby b/formal/psl_logical_implication.sby index 2d06026..ebc053b 100644 --- a/formal/psl_logical_implication.sby +++ b/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] diff --git a/formal/psl_never.sby b/formal/psl_never.sby index 76b6483..e597934 100644 --- a/formal/psl_never.sby +++ b/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] diff --git a/formal/psl_next.sby b/formal/psl_next.sby index 4c51115..7c08683 100644 --- a/formal/psl_next.sby +++ b/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] diff --git a/formal/psl_next_3.sby b/formal/psl_next_3.sby index 07eab26..613a12c 100644 --- a/formal/psl_next_3.sby +++ b/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] diff --git a/formal/psl_next_a.sby b/formal/psl_next_a.sby index 5e3e8e4..ffef88f 100644 --- a/formal/psl_next_a.sby +++ b/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] diff --git a/formal/psl_next_e.sby b/formal/psl_next_e.sby index 5da59d5..7d2d386 100644 --- a/formal/psl_next_e.sby +++ b/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] diff --git a/formal/psl_next_event.sby b/formal/psl_next_event.sby index cd5a419..d5d040d 100644 --- a/formal/psl_next_event.sby +++ b/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] diff --git a/formal/psl_next_event_4.sby b/formal/psl_next_event_4.sby index 21a9cb9..51fb92c 100644 --- a/formal/psl_next_event_4.sby +++ b/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] diff --git a/formal/psl_next_event_a.sby b/formal/psl_next_event_a.sby index 34084b1..2052748 100644 --- a/formal/psl_next_event_a.sby +++ b/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] diff --git a/formal/psl_next_event_e.sby b/formal/psl_next_event_e.sby index c706f56..a59d43f 100644 --- a/formal/psl_next_event_e.sby +++ b/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] diff --git a/formal/psl_sere.sby b/formal/psl_sere.sby index 01fcd94..008957d 100644 --- a/formal/psl_sere.sby +++ b/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] diff --git a/formal/psl_sere_non_overlapping_suffix_impl.sby b/formal/psl_sere_non_overlapping_suffix_impl.sby index a99eb89..f504ac8 100644 --- a/formal/psl_sere_non_overlapping_suffix_impl.sby +++ b/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] diff --git a/formal/psl_sere_overlapping_suffix_impl.sby b/formal/psl_sere_overlapping_suffix_impl.sby index b3c2e4c..92d4611 100644 --- a/formal/psl_sere_overlapping_suffix_impl.sby +++ b/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] diff --git a/formal/psl_until.sby b/formal/psl_until.sby index 6d4d0b3..76b5f7b 100644 --- a/formal/psl_until.sby +++ b/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]