From 164d834a13dc992f541d0bed50bcaacf3958249c Mon Sep 17 00:00:00 2001 From: tmeissner Date: Thu, 14 Oct 2021 12:33:03 +0200 Subject: Add test for PSL declarations in inline PSL --- testsuite/synth/psl01/property0.vhdl | 30 ++++++++++++++++++++++++++++++ testsuite/synth/psl01/sequence0.vhdl | 32 ++++++++++++++++++++++++++++++++ testsuite/synth/psl01/testsuite.sh | 2 +- 3 files changed, 63 insertions(+), 1 deletion(-) create mode 100644 testsuite/synth/psl01/property0.vhdl create mode 100644 testsuite/synth/psl01/sequence0.vhdl (limited to 'testsuite') diff --git a/testsuite/synth/psl01/property0.vhdl b/testsuite/synth/psl01/property0.vhdl new file mode 100644 index 000000000..14655365a --- /dev/null +++ b/testsuite/synth/psl01/property0.vhdl @@ -0,0 +1,30 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity property0 is + port (clk, rst: std_logic; + cnt : out unsigned(3 downto 0)); +end property0; + +architecture behav of property0 is + signal val : unsigned (3 downto 0); + default clock is rising_edge(clk); +begin + process(clk) + begin + if rising_edge(clk) then + if rst = '1' then + val <= (others => '0'); + else + val <= val + 1; + end if; + end if; + end process; + cnt <= val; + + property prop is always {val = 8} |=> {val = 9} abort rst; + + assert prop; + +end behav; \ No newline at end of file diff --git a/testsuite/synth/psl01/sequence0.vhdl b/testsuite/synth/psl01/sequence0.vhdl new file mode 100644 index 000000000..67edc7723 --- /dev/null +++ b/testsuite/synth/psl01/sequence0.vhdl @@ -0,0 +1,32 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity sequence0 is + port (clk, rst: std_logic; + cnt : out unsigned(3 downto 0)); +end sequence0; + +architecture behav of sequence0 is + signal val : unsigned (3 downto 0); + default clock is rising_edge(clk); +begin + process(clk) + begin + if rising_edge(clk) then + if rst = '1' then + val <= (others => '0'); + else + val <= val + 1; + end if; + end if; + end process; + cnt <= val; + + sequence seq is {val = 8; val = 9}; + + assert always seq |=> {val = 10} abort rst; + + cover seq; + +end behav; diff --git a/testsuite/synth/psl01/testsuite.sh b/testsuite/synth/psl01/testsuite.sh index fe19e38c6..d6fe7abb9 100755 --- a/testsuite/synth/psl01/testsuite.sh +++ b/testsuite/synth/psl01/testsuite.sh @@ -4,7 +4,7 @@ GHDL_STD_FLAGS=--std=08 -for f in restrict1 restrict2 assume1 assume2 assert1 cover1 cover2; do +for f in restrict1 restrict2 assume1 assume2 assert1 cover1 cover2 property0 sequence0; do synth -fpsl $f.vhdl -e $f > syn_$f.vhdl analyze syn_$f.vhdl done -- cgit v1.2.3