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

@@ -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)

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

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;