From 2cec27d08176be4ed7788582014dcedcf15d69fd Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Mon, 8 Jun 2020 11:19:35 +0200
Subject: [PATCH] Add fell() example to formal tests after it was implemented
 by ghdl/ghdl#1357

---
 README.md        |  3 ++-
 formal/tests.mk  |  3 ++-
 src/psl_fell.vhd | 25 +++++++++++++++++++------
 3 files changed, 23 insertions(+), 8 deletions(-)

diff --git a/README.md b/README.md
index e32e542..74ec88c 100644
--- a/README.md
+++ b/README.md
@@ -63,12 +63,13 @@ The next lists will grow during further development
 * `prev()` function (Synthesis only, see [prev() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_prev.vhd))
 * `stable()` function (Synthesis only, see [stable() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_stable.vhd))
 * `rose()` function (Synthesis only, see [rose() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_rose.vhd))
+* `fell()` function (Synthesis only, see [fell() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_fell.vhd))
 
 ## Not yet supported by GHDL:
 
 * `forall` statement
 * Synthesis of strong operator versions
-* PSL functions (`prev()`, `stable()` & `rose()` are implemented for synthesis)
+* PSL functions (`prev()`, `stable()`,`rose()` & `fell()` are implemented for synthesis)
 
 ## Under investigation
 
diff --git a/formal/tests.mk b/formal/tests.mk
index 6e3bd90..6d1217c 100644
--- a/formal/tests.mk
+++ b/formal/tests.mk
@@ -28,4 +28,5 @@ psl_sere_concat \
 psl_sere_fusion \
 psl_prev \
 psl_stable \
-psl_rose
+psl_rose \
+psl_fell
diff --git a/src/psl_fell.vhd b/src/psl_fell.vhd
index 293a4ae..d65eea0 100644
--- a/src/psl_fell.vhd
+++ b/src/psl_fell.vhd
@@ -13,21 +13,28 @@ end entity psl_fell;
 
 architecture psl of psl_fell is
 
-  signal a, b : std_logic;
+  signal a, b, c : std_logic;
 
 begin
 
 
   --                              01234567890
-  SEQ_A : sequencer generic map ("_-__-_---__") port map (clk, a);
-  SEQ_B : sequencer generic map ("__-__-___-_") port map (clk, b);
+  SEQ_A : sequencer generic map ("--__-_---__") port map (clk, a);
+  SEQ_B : sequencer generic map ("_-__-_---__") port map (clk, b);
+  SEQ_C : sequencer generic map ("__-__-___-_") port map (clk, c);
 
 
   -- All is sensitive to rising edge of clk
   default clock is rising_edge(clk);
 
   -- This assertion holds
-  FELL_0_a : assert always (fell(a) -> b);
+  FELL_0_a : assert always (fell(a) -> c);
+
+  -- This assertion holds
+  FELL_1_a : assert always {a; not a} |-> fell(a);
+
+  -- This assertion holds
+  FELL_2_a : assert always (fell(a) -> (prev(a) and not a));
 
   -- Workaround needed before fell() is implemented
   -- With VHDL glue logic generating the
@@ -41,11 +48,17 @@ begin
         a_prev <= a;
       end if;
     end process;
-    FELL_1_a : assert always (not a and a_prev -> b);
+    FELL_3_a : assert always (not a and a_prev -> c);
   end block d_reg;
 
   -- Another workaround by using simple SERE concatenation on LHS
-  FELL_2_a : assert always {a; not a} |-> b;
+  FELL_4_a : assert always {a; not a} |-> c;
+
+  -- This assertion doesn't in formal tests
+  -- in the 1st cycle. Problem is the value of
+  -- a in the 0th cycle. So fell() can be safely
+  -- used from the 2nd cycle on only
+  FELL_5_a : assert always (fell(b) -> c);
 
   -- Stop simulation after longest running sequencer is finished
   -- Simulation only code by using pragmas