diff options
Diffstat (limited to 'tests/sva')
-rw-r--r-- | tests/sva/.gitignore | 2 | ||||
-rw-r--r-- | tests/sva/Makefile | 8 | ||||
-rw-r--r-- | tests/sva/runtest.sh | 37 | ||||
-rw-r--r-- | tests/sva/vhdlpsl00.vhd | 34 |
4 files changed, 64 insertions, 17 deletions
diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore index 254013047..cc254049a 100644 --- a/tests/sva/.gitignore +++ b/tests/sva/.gitignore @@ -3,3 +3,5 @@ /*_pass /*_fail /*.ok +/vhdlpsl[0-9][0-9] +/vhdlpsl[0-9][0-9].sby diff --git a/tests/sva/Makefile b/tests/sva/Makefile index c2ee5e9d8..1b217f746 100644 --- a/tests/sva/Makefile +++ b/tests/sva/Makefile @@ -1,13 +1,13 @@ -TESTS = $(basename $(wildcard *.sv)) +TESTS = $(sort $(basename $(wildcard *.sv)) $(basename $(wildcard *.vhd))) all: $(addsuffix .ok,$(TESTS)) -%.ok: %.sv - bash runtest.sh $< +%.ok: + bash runtest.sh $@ clean: - rm -rf $(addsuffix .ok,$(TESTS)) + rm -rf $(addsuffix .ok,$(TESTS)) $(addsuffix .sby,$(TESTS)) $(TESTS) rm -rf $(addsuffix _pass.sby,$(TESTS)) $(addsuffix _pass,$(TESTS)) rm -rf $(addsuffix _fail.sby,$(TESTS)) $(addsuffix _fail,$(TESTS)) diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh index 004a172ba..35c95a3e0 100644 --- a/tests/sva/runtest.sh +++ b/tests/sva/runtest.sh @@ -2,8 +2,10 @@ set -ex -prefix=${1%.sv} -test -f $prefix.sv +prefix=${1%.ok} +prefix=${prefix%.sv} +prefix=${prefix%.vhd} +test -f $prefix.sv -o -f $prefix.vhd generate_sby() { cat <<- EOT @@ -18,14 +20,16 @@ generate_sby() { [script] EOT - if [ "$1" = "fail" ]; then - echo "verific -sv ${prefix}_fail.sv" - else - echo "verific -sv $prefix.sv" + if [ -f $prefix.sv ]; then + if [ "$1" = "fail" ]; then + echo "verific -sv ${prefix}_fail.sv" + else + echo "verific -sv $prefix.sv" + fi fi if [ -f $prefix.vhd ]; then - echo "verific -vhdl2008 $prefix.vhd" + echo "verific -vhdpsl $prefix.vhd" fi cat <<- EOT @@ -33,9 +37,12 @@ generate_sby() { prep -top top [files] - $prefix.sv EOT + if [ -f $prefix.sv ]; then + echo "$prefix.sv" + fi + if [ -f $prefix.vhd ]; then echo "$prefix.vhd" fi @@ -50,11 +57,15 @@ generate_sby() { fi } -generate_sby pass > ${prefix}_pass.sby -generate_sby fail > ${prefix}_fail.sby - -sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby -sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby +if [ -f $prefix.sv ]; then + generate_sby pass > ${prefix}_pass.sby + generate_sby fail > ${prefix}_fail.sby + sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby + sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby +else + generate_sby pass > ${prefix}.sby + sby --yosys $PWD/../../yosys -f ${prefix}.sby +fi touch $prefix.ok diff --git a/tests/sva/vhdlpsl00.vhd b/tests/sva/vhdlpsl00.vhd new file mode 100644 index 000000000..6d765d5a9 --- /dev/null +++ b/tests/sva/vhdlpsl00.vhd @@ -0,0 +1,34 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.std_logic_unsigned.all; +use ieee.numeric_std.all; + +entity top is + port ( + clk : in std_logic; + rst : in std_logic; + up : in std_logic; + down : in std_logic; + cnt : buffer std_logic_vector(7 downto 0) + ); +end entity; + +architecture rtl of top is +begin + process (clk) begin + if rising_edge(clk) then + if rst = '1' then + cnt <= std_logic_vector(to_unsigned(0, 8)); + elsif up = '1' then + cnt <= cnt + std_logic_vector(to_unsigned(1, 8)); + elsif down = '1' then + cnt <= cnt - std_logic_vector(to_unsigned(1, 8)); + end if; + end if; + end process; + + -- PSL default clock is (rising_edge(clk)); + -- PSL assume always ( down -> not up ); + -- PSL assert always ( up |=> (cnt = prev(cnt) + std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1'; + -- PSL assert always ( down |=> (cnt = prev(cnt) - std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1'; +end architecture; |