diff options
Diffstat (limited to 'testsuite')
-rw-r--r-- | testsuite/synth/psl01/assert1.vhdl | 27 | ||||
-rw-r--r-- | testsuite/synth/psl01/assume1.vhdl | 27 | ||||
-rw-r--r-- | testsuite/synth/psl01/restrict1.vhdl | 27 | ||||
-rwxr-xr-x | testsuite/synth/psl01/testsuite.sh | 7 |
4 files changed, 86 insertions, 2 deletions
diff --git a/testsuite/synth/psl01/assert1.vhdl b/testsuite/synth/psl01/assert1.vhdl new file mode 100644 index 000000000..13e44a1e8 --- /dev/null +++ b/testsuite/synth/psl01/assert1.vhdl @@ -0,0 +1,27 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity assert1 is + port (clk, rst: std_logic; + cnt : out unsigned(3 downto 0)); +end assert1; + +architecture behav of assert1 is + signal val : unsigned (3 downto 0); +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; + + --psl default clock is rising_edge(clk); + --psl assert always val /= 5 or rst = '1'; +end behav; diff --git a/testsuite/synth/psl01/assume1.vhdl b/testsuite/synth/psl01/assume1.vhdl new file mode 100644 index 000000000..0bc54c56f --- /dev/null +++ b/testsuite/synth/psl01/assume1.vhdl @@ -0,0 +1,27 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity assume1 is + port (clk, rst: std_logic; + cnt : out unsigned(3 downto 0)); +end assume1; + +architecture behav of assume1 is + signal val : unsigned (3 downto 0); +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; + + --psl default clock is rising_edge(clk); + --psl assume always val < 50; +end behav; diff --git a/testsuite/synth/psl01/restrict1.vhdl b/testsuite/synth/psl01/restrict1.vhdl new file mode 100644 index 000000000..b932acc9a --- /dev/null +++ b/testsuite/synth/psl01/restrict1.vhdl @@ -0,0 +1,27 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity restrict1 is + port (clk, rst: std_logic; + cnt : out unsigned(3 downto 0)); +end restrict1; + +architecture behav of restrict1 is + signal val : unsigned (3 downto 0); +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; + + --psl default clock is rising_edge (clk); + --psl restrict {rst; (not rst)[*]}; +end behav; diff --git a/testsuite/synth/psl01/testsuite.sh b/testsuite/synth/psl01/testsuite.sh index e6d4050e6..4c43382b6 100755 --- a/testsuite/synth/psl01/testsuite.sh +++ b/testsuite/synth/psl01/testsuite.sh @@ -3,8 +3,11 @@ . ../../testenv.sh GHDL_STD_FLAGS=--std=08 -synth -fpsl hello.vhdl -e hello > syn_hello.vhdl -analyze syn_hello.vhdl + +for f in restrict1 assume1 assert1; do + synth -fpsl $f.vhdl -e $f > syn_$f.vhdl + analyze syn_$f.vhdl +done clean echo "Test successful" |