From 7a8a3743fe7e29a44ccf9068c0af7cfc68869aa7 Mon Sep 17 00:00:00 2001
From: Tristan Gingold <tgingold@free.fr>
Date: Tue, 9 Feb 2021 21:02:22 +0100
Subject: testsuite/synth: adjust tests for issue#662

---
 testsuite/synth/issue662/psl_fell_err1.vhdl  | 16 ++++++++++++++++
 testsuite/synth/issue662/psl_onehot.vhdl     |  6 +-----
 testsuite/synth/issue662/psl_onehot0.vhdl    |  6 +-----
 testsuite/synth/issue662/psl_onehot_err.vhdl | 28 ++++++++++++++++++++++++++++
 testsuite/synth/issue662/tb_psl_onehot.vhdl  |  5 +----
 testsuite/synth/issue662/tb_psl_onehot0.vhdl |  5 +----
 testsuite/synth/issue662/testsuite.sh        |  3 +++
 7 files changed, 51 insertions(+), 18 deletions(-)
 create mode 100644 testsuite/synth/issue662/psl_fell_err1.vhdl
 create mode 100644 testsuite/synth/issue662/psl_onehot_err.vhdl

diff --git a/testsuite/synth/issue662/psl_fell_err1.vhdl b/testsuite/synth/issue662/psl_fell_err1.vhdl
new file mode 100644
index 000000000..6ef80a0a5
--- /dev/null
+++ b/testsuite/synth/issue662/psl_fell_err1.vhdl
@@ -0,0 +1,16 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity psl_fell1 is
+  port (clk, a, b : in std_logic
+  );
+end entity psl_fell1;
+
+
+architecture psl of psl_fell1 is
+begin
+
+  -- This assertion holds
+  FELL_0_a : assert always {a; not a} |-> fell(a);
+
+end architecture psl;
diff --git a/testsuite/synth/issue662/psl_onehot.vhdl b/testsuite/synth/issue662/psl_onehot.vhdl
index feaa784df..97753a17b 100644
--- a/testsuite/synth/issue662/psl_onehot.vhdl
+++ b/testsuite/synth/issue662/psl_onehot.vhdl
@@ -4,8 +4,7 @@ use ieee.numeric_std.all;
 
 entity psl_onehot is
   port (clk  : in std_logic;
-        a, b : in std_logic_vector(3 downto 0);
-        c    : in natural range 0 to 15
+        a, b : in std_logic_vector(3 downto 0)
   );
 end entity psl_onehot;
 
@@ -22,7 +21,4 @@ begin
   -- This assertion fails at cycle 12
   ONEHOT_1_a : assert always onehot(b);
 
-  -- This assertion fails at cycle 12
-  ONEHOT_2_a : assert always onehot(c);
-
 end architecture psl;
diff --git a/testsuite/synth/issue662/psl_onehot0.vhdl b/testsuite/synth/issue662/psl_onehot0.vhdl
index edd4361c8..8c9b2e805 100644
--- a/testsuite/synth/issue662/psl_onehot0.vhdl
+++ b/testsuite/synth/issue662/psl_onehot0.vhdl
@@ -3,8 +3,7 @@ use ieee.std_logic_1164.all;
 
 entity psl_onehot0 is
   port (clk  : in std_logic;
-        a, b : in std_logic_vector(3 downto 0);
-        c    : in natural range 0 to 15
+        a, b : in std_logic_vector(3 downto 0)
   );
 end entity psl_onehot0;
 
@@ -21,7 +20,4 @@ begin
   -- This assertion fails at cycle 15
   ONEHOT0_1_a : assert always onehot0(b);
 
-  -- This assertion fails at cycle 15
-  ONEHOT0_2_a : assert always onehot(c);
-
 end architecture psl;
diff --git a/testsuite/synth/issue662/psl_onehot_err.vhdl b/testsuite/synth/issue662/psl_onehot_err.vhdl
new file mode 100644
index 000000000..c259ce79d
--- /dev/null
+++ b/testsuite/synth/issue662/psl_onehot_err.vhdl
@@ -0,0 +1,28 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity psl_onehot_err is
+  port (clk  : in std_logic;
+        a, b : in std_logic_vector(3 downto 0);
+        c    : in natural range 0 to 15
+  );
+end entity psl_onehot_err;
+
+
+architecture psl of psl_onehot_err is
+begin
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- This assertion holds
+  ONEHOT_0_a : assert always onehot(a);
+
+  -- This assertion fails at cycle 12
+  ONEHOT_1_a : assert always onehot(b);
+
+  -- This assertion fails at cycle 12
+  ONEHOT_2_a : assert always onehot(c);
+
+end architecture psl;
diff --git a/testsuite/synth/issue662/tb_psl_onehot.vhdl b/testsuite/synth/issue662/tb_psl_onehot.vhdl
index 10b5d8c73..0bf60bf5d 100644
--- a/testsuite/synth/issue662/tb_psl_onehot.vhdl
+++ b/testsuite/synth/issue662/tb_psl_onehot.vhdl
@@ -51,12 +51,11 @@ architecture psl of tb_psl_onehot is
   end hseq;
 
   signal a, b : std_logic_vector(3 downto 0) := x"0";
-  signal c    : natural range 0 to 15 := 0;
   signal clk  : std_logic := '1';
 
 begin
 
-  dut: entity work.psl_onehot port map (clk, a, b, c);
+  dut: entity work.psl_onehot port map (clk, a, b);
 
   clk <= not clk after 500 ps;
 
@@ -64,6 +63,4 @@ begin
   SEQ_A : hseq ("111222444888888", clk, a);
   SEQ_B : hseq ("111222444888999", clk, b);
 
-  c <= to_integer(unsigned(b));
-
 end architecture psl;
diff --git a/testsuite/synth/issue662/tb_psl_onehot0.vhdl b/testsuite/synth/issue662/tb_psl_onehot0.vhdl
index 2f51ba020..5a04043b6 100644
--- a/testsuite/synth/issue662/tb_psl_onehot0.vhdl
+++ b/testsuite/synth/issue662/tb_psl_onehot0.vhdl
@@ -51,12 +51,11 @@ architecture psl of tb_psl_onehot0 is
   end hseq;
 
   signal a, b : std_logic_vector(3 downto 0) := x"0";
-  signal c    : natural range 0 to 15 := 0;
   signal clk  : std_logic := '1';
 
 begin
 
-  dut: entity work.psl_onehot0 port map (clk, a, b, c);
+  dut: entity work.psl_onehot0 port map (clk, a, b);
 
   clk <= not clk after 500 ps;
 
@@ -64,6 +63,4 @@ begin
   SEQ_A : hseq ("000111222444888888", clk, a);
   SEQ_B : hseq ("000111222444888fff", clk, b);
 
-  c <= to_integer(unsigned(b));
-
 end architecture psl;
diff --git a/testsuite/synth/issue662/testsuite.sh b/testsuite/synth/issue662/testsuite.sh
index cf8647e76..2ff5d4a7c 100755
--- a/testsuite/synth/issue662/testsuite.sh
+++ b/testsuite/synth/issue662/testsuite.sh
@@ -11,6 +11,9 @@ for test in psl_prev psl_stable psl_rose psl_fell psl_onehot psl_onehot0; do
   elab_simulate tb_${test} --stop-time=10ns --asserts=disable-at-0 --assert-level=error
 done
 
+analyze_failure psl_fell_err1.vhdl
+analyze_failure psl_onehot_err.vhdl
+
 clean
 
 echo "Test successful"
-- 
cgit v1.2.3