From 9993f167fb9a7e45ea233447d9257df04339c250 Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Sat, 6 Jun 2020 19:52:50 +0200
Subject: testsuite/synth: add a test of PSL built-in function fell() for #662

---
 testsuite/synth/issue662/psl_fell.vhdl    | 25 +++++++++++++++++++++
 testsuite/synth/issue662/tb_psl_fell.vhdl | 37 +++++++++++++++++++++++++++++++
 testsuite/synth/issue662/testsuite.sh     |  2 +-
 3 files changed, 63 insertions(+), 1 deletion(-)
 create mode 100644 testsuite/synth/issue662/psl_fell.vhdl
 create mode 100644 testsuite/synth/issue662/tb_psl_fell.vhdl

(limited to 'testsuite')

diff --git a/testsuite/synth/issue662/psl_fell.vhdl b/testsuite/synth/issue662/psl_fell.vhdl
new file mode 100644
index 000000000..a3261a923
--- /dev/null
+++ b/testsuite/synth/issue662/psl_fell.vhdl
@@ -0,0 +1,25 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity psl_fell is
+  port (clk, a, b : in std_logic
+  );
+end entity psl_fell;
+
+
+architecture psl of psl_fell is
+begin
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- This assertion holds
+  FELL_0_a : assert always {a; not a} |-> fell(a);
+
+  -- This assertion holds
+  FELL_1_a : assert always (fell(a) -> (prev(a) = '1' and a = '0'));
+
+  -- This assertion should fail at cycle 11
+  FELL_2_a : assert always fell(a) -> b;
+
+end architecture psl;
diff --git a/testsuite/synth/issue662/tb_psl_fell.vhdl b/testsuite/synth/issue662/tb_psl_fell.vhdl
new file mode 100644
index 000000000..fc1c975b5
--- /dev/null
+++ b/testsuite/synth/issue662/tb_psl_fell.vhdl
@@ -0,0 +1,37 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+entity tb_psl_fell is
+end entity tb_psl_fell;
+
+
+architecture psl of tb_psl_fell is
+
+  procedure seq (s : string; signal clk : std_logic; signal o : out std_logic)
+  is
+  begin
+    for i in s'range loop
+      wait until rising_edge(clk);
+      case s(i) is
+        when '0' | '_' => o <= '0';
+        when '1' | '-' => o <= '1';
+        when others    => o <= 'X';
+      end case;
+    end loop;
+    wait;
+  end seq;
+
+  signal a, b : std_logic := '0';
+  signal clk  : std_logic := '1';
+
+begin
+
+  dut: entity work.psl_fell port map (clk, a, b);
+
+  clk <= not clk after 500 ps;
+
+  --             012345678901234
+  SEQ_A :  seq ("--_--___---__--", clk, a);
+  SEQ_B :  seq ("__-__-______-__", clk, b);
+
+end architecture psl;
diff --git a/testsuite/synth/issue662/testsuite.sh b/testsuite/synth/issue662/testsuite.sh
index 1047b853e..5186799d1 100755
--- a/testsuite/synth/issue662/testsuite.sh
+++ b/testsuite/synth/issue662/testsuite.sh
@@ -4,7 +4,7 @@
 
 GHDL_STD_FLAGS=--std=08
 
-for test in psl_prev psl_stable psl_rose; do
+for test in psl_prev psl_stable psl_rose psl_fell; do
   synth_analyze $test
   analyze tb_${test}.vhdl
   elab_simulate_failure tb_${test} --stop-time=20ns --asserts=disable-at-0 --assert-level=error
-- 
cgit v1.2.3