diff options
Diffstat (limited to 'testsuite/synth/psl01')
-rw-r--r-- | testsuite/synth/psl01/cover1.vhdl | 27 | ||||
-rw-r--r-- | testsuite/synth/psl01/cover2.vhdl | 27 | ||||
-rw-r--r-- | testsuite/synth/psl01/hello.vhdl | 1 | ||||
-rwxr-xr-x | testsuite/synth/psl01/testsuite.sh | 2 |
4 files changed, 56 insertions, 1 deletions
diff --git a/testsuite/synth/psl01/cover1.vhdl b/testsuite/synth/psl01/cover1.vhdl new file mode 100644 index 000000000..8512b3b18 --- /dev/null +++ b/testsuite/synth/psl01/cover1.vhdl @@ -0,0 +1,27 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity cover1 is + port (clk, rst: std_logic; + cnt : out unsigned(3 downto 0)); +end cover1; + +architecture behav of cover1 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 cover {val = 10}; +end behav; diff --git a/testsuite/synth/psl01/cover2.vhdl b/testsuite/synth/psl01/cover2.vhdl new file mode 100644 index 000000000..d04757694 --- /dev/null +++ b/testsuite/synth/psl01/cover2.vhdl @@ -0,0 +1,27 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity cover2 is + port (clk, rst: std_logic; + cnt : out unsigned(3 downto 0)); +end cover2; + +architecture behav of cover2 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; + + cover {val = 10}; +end behav; diff --git a/testsuite/synth/psl01/hello.vhdl b/testsuite/synth/psl01/hello.vhdl index 6676b883a..325f7f078 100644 --- a/testsuite/synth/psl01/hello.vhdl +++ b/testsuite/synth/psl01/hello.vhdl @@ -26,4 +26,5 @@ begin --psl restrict {rst; (not rst)[*]}; --psl assert always val /= 5 abort rst; --psl assume always val < 10; + --psl cover {val = 10}; end behav; diff --git a/testsuite/synth/psl01/testsuite.sh b/testsuite/synth/psl01/testsuite.sh index 7fd87887f..7707566f7 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; do +for f in restrict1 restrict2 assume1 assume2 assert1 cover1 cover2; do synth -fpsl $f.vhdl -e $f > syn_$f.vhdl analyze syn_$f.vhdl done |