testsuite/synth: add testcase for psl.

7 files changed, 79 insertions, 0 deletions

diff --git a/testsuite/synth/fsm03/assert1.psl b/testsuite/synth/fsm03/assert1.psl
new file mode 100644
index 000000000..54cbb7ddb
--- /dev/null
+++ b/testsuite/synth/fsm03/assert1.psl
@@ -0,0 +1,5 @@
+vunit assert1 (ent)
+{
+  default clock is rising_edge(clk);
+  assert always req -> eventually! ack;
+}
diff --git a/testsuite/synth/fsm03/assert2.psl b/testsuite/synth/fsm03/assert2.psl
new file mode 100644
index 000000000..498adb2fb
--- /dev/null
+++ b/testsuite/synth/fsm03/assert2.psl
@@ -0,0 +1,5 @@
+vunit assert1 (ent)
+{
+  default clock is rising_edge(clk);
+  assert always {val; req} |-> eventually! ack;
+}
diff --git a/testsuite/synth/fsm03/assert3.psl b/testsuite/synth/fsm03/assert3.psl
new file mode 100644
index 000000000..e44e606d4
--- /dev/null
+++ b/testsuite/synth/fsm03/assert3.psl
@@ -0,0 +1,5 @@
+vunit assert3 (ent)
+{
+  default clock is rising_edge(clk);
+  my_cond: assert always {val; req} |=> eventually! ack;
+}
diff --git a/testsuite/synth/fsm03/assert4.psl b/testsuite/synth/fsm03/assert4.psl
new file mode 100644
index 000000000..a846b18b9
--- /dev/null
+++ b/testsuite/synth/fsm03/assert4.psl
@@ -0,0 +1,10 @@
+vunit assert3 (ent)
+{
+  default clock is rising_edge(clk);
+  function get_nval (v : std_logic) return std_logic is
+  begin
+    return not v;
+  end get_nval;
+  --  signal nval : std_logic;
+  my_cond: assert always {get_nval (val); req} |=> eventually! ack;
+}
diff --git a/testsuite/synth/fsm03/assert5.psl b/testsuite/synth/fsm03/assert5.psl
new file mode 100644
index 000000000..9edfc174f
--- /dev/null
+++ b/testsuite/synth/fsm03/assert5.psl
@@ -0,0 +1,6 @@
+vunit assert5 (ent)
+{
+  default clock is rising_edge(clk);
+  --my_cond: assert always (({req} |=> {ack}) abort val = '1');
+  my_cond: assert always ({req} |=> {ack});
+}
diff --git a/testsuite/synth/fsm03/ent.vhdl b/testsuite/synth/fsm03/ent.vhdl
new file mode 100644
index 000000000..46adc93d8
--- /dev/null
+++ b/testsuite/synth/fsm03/ent.vhdl
@@ -0,0 +1,31 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity ent is
+  port (
+   clk : std_logic;
+   req : std_logic;
+   val : std_logic;
+   ack : out std_logic);
+end ent;
+
+architecture behav of ent is
+  signal cnt : natural range 0 to 5;
+begin
+  process (clk)
+  begin
+    if rising_edge(clk) then
+      if cnt < 5 then
+        cnt <= cnt + 1;
+      else
+        cnt <= 0;
+      end if;
+      if req = '1' and cnt = 0 then
+        ack <= '1';
+      else
+        ack <= '0';
+      end if;
+    end if;
+  end process;
+end behav;
+
diff --git a/testsuite/synth/fsm03/testsuite.sh b/testsuite/synth/fsm03/testsuite.sh
new file mode 100755
index 000000000..31b338371
--- /dev/null
+++ b/testsuite/synth/fsm03/testsuite.sh
@@ -0,0 +1,17 @@
+#! /bin/sh
+
+exit 0
+. ../../testenv.sh
+
+for t in rom1 dpram1 dpram2 dpram3; do
+    analyze $t.vhdl tb_$t.vhdl
+    elab_simulate tb_$t
+    clean
+
+    synth $t.vhdl -e $t > syn_$t.vhdl
+    analyze syn_$t.vhdl tb_$t.vhdl
+    elab_simulate tb_$t --ieee-asserts=disable-at-0
+    clean
+done
+
+echo "Test successful"