From 0a044db5d0b5aaa3eddd8621d2b50de602dc31e3 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Mon, 18 May 2020 12:42:25 +0200 Subject: [PATCH] Fixed entity & file names of [=] examples --- README.md | 2 +- .../psl_sere_consecutive_repeat_repetition.sby | 18 ------------------ ..._sere_non_consecutive_repeat_repetition.sby | 18 ++++++++++++++++++ formal/tests.mk | 3 ++- ...sere_non_consecutive_repeat_repetition.vhd} | 6 +++--- 5 files changed, 24 insertions(+), 23 deletions(-) delete mode 100644 formal/psl_sere_consecutive_repeat_repetition.sby create mode 100644 formal/psl_sere_non_consecutive_repeat_repetition.sby rename src/{psl_sere_consecutive_repeat_repetition.vhd => psl_sere_non_consecutive_repeat_repetition.vhd} (92%) diff --git a/README.md b/README.md index e35a7f9..f522d5f 100644 --- a/README.md +++ b/README.md @@ -58,7 +58,7 @@ The next lists will grow during further development * Synthesis of strong operator versions * SERE goto repetition operator ([->], [->n], [->i to j]) -## PSL features supported by GHDL, behaviour under investigation +## PSL features under investigation * before_ operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd) * next_event_a[i to j] operator (Behaviour currently under investigation) diff --git a/formal/psl_sere_consecutive_repeat_repetition.sby b/formal/psl_sere_consecutive_repeat_repetition.sby deleted file mode 100644 index 0034c18..0000000 --- a/formal/psl_sere_consecutive_repeat_repetition.sby +++ /dev/null @@ -1,18 +0,0 @@ -[tasks] -bmc - -[options] -depth 25 -bmc: mode bmc - -[engines] -bmc: smtbmc z3 - -[script] -bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere_consecutive_repeat_repetition.vhd -e psl_sere_consecutive_repeat_repetition -prep -top psl_sere_consecutive_repeat_repetition - -[files] -../src/pkg.vhd -../src/sequencer.vhd -../src/psl_sere_consecutive_repeat_repetition.vhd diff --git a/formal/psl_sere_non_consecutive_repeat_repetition.sby b/formal/psl_sere_non_consecutive_repeat_repetition.sby new file mode 100644 index 0000000..7d38009 --- /dev/null +++ b/formal/psl_sere_non_consecutive_repeat_repetition.sby @@ -0,0 +1,18 @@ +[tasks] +bmc + +[options] +depth 25 +bmc: mode bmc + +[engines] +bmc: smtbmc z3 + +[script] +bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere_non_consecutive_repeat_repetition.vhd -e psl_sere_non_consecutive_repeat_repetition +prep -top psl_sere_non_consecutive_repeat_repetition + +[files] +../src/pkg.vhd +../src/sequencer.vhd +../src/psl_sere_non_consecutive_repeat_repetition.vhd diff --git a/formal/tests.mk b/formal/tests.mk index c68d8db..470cfc7 100644 --- a/formal/tests.mk +++ b/formal/tests.mk @@ -17,4 +17,5 @@ psl_sere \ psl_sere_overlapping_suffix_impl \ psl_sere_non_overlapping_suffix_impl \ psl_sere_consecutive_repetition \ -psl_sere_consecutive_repeat_repetition +psl_sere_non_consecutive_repeat_repetition \ +psl_sere_non_consecutive_goto_repetition diff --git a/src/psl_sere_consecutive_repeat_repetition.vhd b/src/psl_sere_non_consecutive_repeat_repetition.vhd similarity index 92% rename from src/psl_sere_consecutive_repeat_repetition.vhd rename to src/psl_sere_non_consecutive_repeat_repetition.vhd index 87a5593..7854244 100644 --- a/src/psl_sere_consecutive_repeat_repetition.vhd +++ b/src/psl_sere_non_consecutive_repeat_repetition.vhd @@ -4,14 +4,14 @@ library ieee; use work.pkg.all; -entity psl_sere_consecutive_repeat_repetition is +entity psl_sere_non_consecutive_repeat_repetition is port ( clk : in std_logic ); -end entity psl_sere_consecutive_repeat_repetition; +end entity psl_sere_non_consecutive_repeat_repetition; -architecture psl of psl_sere_consecutive_repeat_repetition is +architecture psl of psl_sere_non_consecutive_repeat_repetition is signal req, busy, done : std_logic;