testsuite/synth: add a test of PSL built-in function stable() for #662

5 files changed, 105 insertions, 11 deletions

diff --git a/testsuite/synth/issue662/issue.vhdl b/testsuite/synth/issue662/psl_prev.vhdl
index 1404b9ecd..c9ddac35b 100644
--- a/testsuite/synth/issue662/issue.vhdl
+++ b/testsuite/synth/issue662/psl_prev.vhdl
@@ -1,12 +1,12 @@
 library ieee;
 use ieee.std_logic_1164.all;
 
-entity issue is
+entity psl_prev is
   port (clk, a, b : std_logic);
-end entity issue;
+end entity psl_prev;
 
 
-architecture psl of issue is
+architecture psl of psl_prev is
 begin
   -- All is sensitive to rising edge of clk
   default clock is rising_edge(clk);
diff --git a/testsuite/synth/issue662/psl_stable.vhdl b/testsuite/synth/issue662/psl_stable.vhdl
new file mode 100644
index 000000000..675cdbd56
--- /dev/null
+++ b/testsuite/synth/issue662/psl_stable.vhdl
@@ -0,0 +1,23 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity psl_stable is
+  port (clk, a, b, c : in std_logic;
+        d         : in std_logic_vector(3 downto 0)
+  );
+end entity psl_stable;
+
+
+architecture psl of psl_stable is
+begin
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- This assertion holds
+  STABLE_0_a : assert always {not a; a} |=> (stable(c) until_ b);
+
+  -- This assertion holds
+  STABLE_1_a : assert always {not a; a} |=> (stable(d) until_ b);
+
+end architecture psl;
diff --git a/testsuite/synth/issue662/tb_issue.vhdl b/testsuite/synth/issue662/tb_psl_prev.vhdl
index c679b059f..edb5dab42 100644
--- a/testsuite/synth/issue662/tb_issue.vhdl
+++ b/testsuite/synth/issue662/tb_psl_prev.vhdl
@@ -1,11 +1,11 @@
 library ieee;
   use ieee.std_logic_1164.all;
 
-entity tb_issue is
-end entity tb_issue;
+entity tb_psl_prev is
+end entity tb_psl_prev;
 
 
-architecture psl of tb_issue is
+architecture psl of tb_psl_prev is
   procedure seq (s : string; signal clk : std_logic; signal o : out std_logic)
   is
   begin
@@ -24,7 +24,7 @@ architecture psl of tb_issue is
   signal clk   : std_logic := '1';
 
 begin
-  dut: entity work.issue port map (clk, a, b);
+  dut: entity work.psl_prev port map (clk, a, b);
 
   clk <= not clk after 500 ps;
 
diff --git a/testsuite/synth/issue662/tb_psl_stable.vhdl b/testsuite/synth/issue662/tb_psl_stable.vhdl
new file mode 100644
index 000000000..b038caf36
--- /dev/null
+++ b/testsuite/synth/issue662/tb_psl_stable.vhdl
@@ -0,0 +1,68 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+entity tb_psl_stable is
+end entity tb_psl_stable;
+
+
+architecture psl of tb_psl_stable 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;
+
+  procedure hseq (s : string; signal clk : std_logic; signal o : out std_logic_vector(3 downto 0))
+  is
+  begin
+    for i in s'range loop
+      wait until rising_edge(clk);
+      case s(i) is
+        when '0' | '_' => o <= x"0";
+        when '1'       => o <= x"1";
+        when '2'       => o <= x"2";
+        when '3'       => o <= x"3";
+        when '4'       => o <= x"4";
+        when '5'       => o <= x"5";
+        when '6'       => o <= x"6";
+        when '7'       => o <= x"7";
+        when '8'       => o <= x"8";
+        when '9'       => o <= x"9";
+        when 'a' | 'A' => o <= x"A";
+        when 'b' | 'B' => o <= x"B";
+        when 'c' | 'C' => o <= x"C";
+        when 'd' | 'D' => o <= x"D";
+        when 'e' | 'E' => o <= x"E";
+        when 'f' | 'F' | '-' => o <= x"F";
+        when others => o <= x"X";
+      end case;
+    end loop;
+    wait;
+  end hseq;
+
+  signal a, b, c : std_logic := '0';
+  signal d       : std_logic_vector(3 downto 0) := x"0";
+  signal clk     : std_logic := '1';
+
+begin
+
+  dut: entity work.psl_stable port map (clk, a, b, c, d);
+
+  clk <= not clk after 500 ps;
+
+  --             012345678901234
+  SEQ_A :  seq ("_--__---____--_", clk, a);
+  SEQ_B :  seq ("__-____-_____-_", clk, b);
+  SEQ_C :  seq ("_--__________-_", clk, c);
+  SEQ_D : hseq ("011006660000000", clk, d);
+
+end architecture psl;
diff --git a/testsuite/synth/issue662/testsuite.sh b/testsuite/synth/issue662/testsuite.sh
index 9f266b29d..62e06f718 100755
--- a/testsuite/synth/issue662/testsuite.sh
+++ b/testsuite/synth/issue662/testsuite.sh
@@ -3,10 +3,13 @@
 . ../../testenv.sh
 
 GHDL_STD_FLAGS=--std=08
-synth_analyze issue
-analyze tb_issue.vhdl
-elab_simulate_failure tb_issue --stop-time=20ns --asserts=disable-at-0 --assert-level=error
-elab_simulate tb_issue --stop-time=10ns --asserts=disable-at-0 --assert-level=error
+
+for test in psl_prev psl_stable; do
+  synth_analyze $test
+  analyze tb_${test}.vhdl
+  elab_simulate_failure tb_${test} --stop-time=20ns --asserts=disable-at-0 --assert-level=error
+  elab_simulate tb_${test} --stop-time=10ns --asserts=disable-at-0 --assert-level=error
+done
 
 clean