From 5c8ced0752f338bb4dd0aee7da3825a6f956e949 Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Mon, 4 May 2020 21:21:44 +0200
Subject: [PATCH] Add examples of before & before_ operators

* Add example for before & before_ operator
* Add formal test for both operators
* Add before operator to supported list
* Add before_ operator to wrong behaviour list
---
 README.md             | 11 ++++++-
 formal/psl_before.sby | 18 ++++++++++
 src/psl_before.vhd    | 76 +++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 104 insertions(+), 1 deletion(-)
 create mode 100644 formal/psl_before.sby
 create mode 100644 src/psl_before.vhd

diff --git a/README.md b/README.md
index 225acea..ccfceed 100644
--- a/README.md
+++ b/README.md
@@ -4,6 +4,10 @@
 
 A collection of examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys).
 
+This is a project with the purpose to get a current state of PSL implementation in GHDL. It probably will find unsupported PSL features, incorrect implemented features or simple bugs like GHDL crashs.
+
+It is also intended for experiments with PSL when learning the language. You can play around with the examples, as they are pretty simple. You can comment out failing assertions if you want to have a sucessful proof os simulation if you want. You can change them to see what happens. Have fun!
+
 
 The next two lists will grow during further development
 
@@ -22,7 +26,8 @@ The next two lists will grow during further development
 * next_event[n] operator
 * until operator
 * until_ operator
-* eventually! operator (simulation, synthesis throws an error)
+* before operator (GHDL crash with a specific property, see psl_before.vhd)
+* eventually! operator (simulation, synthesis produces a GHDL crash, see psl_eventually.vhd)
 
 ## PSL features not yet supported by GHDL:
 
@@ -30,3 +35,7 @@ The next two lists will grow during further development
 * next_e[i:j] operator
 * next_event_a[i:j] operator
 * next_event_e[i:j] operator
+
+## PSL features supported by GHDL but with wrong behaviour
+
+* before_ operator (Overlapping between left & right side not working, see psl_before.vhd)
diff --git a/formal/psl_before.sby b/formal/psl_before.sby
new file mode 100644
index 0000000..c95d7c7
--- /dev/null
+++ b/formal/psl_before.sby
@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_before.vhd -e psl_before
+prep -top psl_before
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_before.vhd
diff --git a/src/psl_before.vhd b/src/psl_before.vhd
new file mode 100644
index 0000000..58d8dea
--- /dev/null
+++ b/src/psl_before.vhd
@@ -0,0 +1,76 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+use work.pkg.all;
+
+
+entity psl_before is
+  port (
+    clk : in std_logic
+  );
+end entity psl_before;
+
+
+architecture psl of psl_before is
+
+  signal a, b : std_logic;
+  signal c, d : std_logic;
+  signal e, f : std_logic;
+
+begin
+
+
+  --                              01234567890
+  SEQ_A : sequencer generic map ("_-____-____") port map (clk, a);
+  SEQ_B : sequencer generic map ("___-_____-_") port map (clk, b);
+
+  --                              01234567890
+  SEQ_C : sequencer generic map ("_-___-_____") port map (clk, c);
+  SEQ_D : sequencer generic map ("_____-___-_") port map (clk, d);
+
+  --                              01234567890
+  SEQ_E : sequencer generic map ("_-____-____") port map (clk, e);
+  SEQ_F : sequencer generic map ("_-_______-_") port map (clk, f);
+
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- This assertion holds
+  BEFORE_0_a : assert always (a -> next (b before a));
+
+  -- This assertion doesn't hold at cycle 5
+  BEFORE_1_a : assert always (c -> next (d before c));
+
+  -- This assertion doesn't hold at cycle 6
+  BEFORE_2_a : assert always (e -> next (f before e));
+
+  -- This is flawed variant of the former assertion
+  -- because even in cycle 1 the b before a property has
+  -- to hold, which is clearly what we want
+  -- This assertion doesn't hold at cycle 1
+  -- Furthermore this assertion leads to a GHDL crash with bug report
+  -- BEFORE_3_a : assert always (a -> (b before a));
+
+  -- This assertion should hold but does not at cycle 3
+  -- Potential GHDL bug?
+  BEFORE_4_a : assert always (a -> next (b before_ a));
+
+  -- This assertion should hold but does not at cycle 9
+  -- Potential GHDL bug?
+   BEFORE_5_a : assert always (c -> next (d before_ c));
+
+  -- This assertion doesn't at cycle 6
+  BEFORE_6_a : assert always (e -> next (f before_ e));
+
+  -- This assertion holds
+  BEFORE_7_a : assert always (a -> (b or next (b before a)));
+
+  -- This assertion doesn't hold at cycle 5
+  BEFORE_8_a : assert always (c -> (d or next (d before c)));
+
+  -- This assertion holds
+  BEFORE_9_a : assert always (e -> (f or next (f before e)));
+
+
+end architecture psl;