Add simple VHDL+PSL example

diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore
index 2540130475446eb61f77231c89ccc9b2e11e0a7a..cc254049ab4c2973ccb592a49c4f453a76270c88 100644 (file)
--- 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 c2ee5e9d862f00ac7e94c96c6c171a158dca537f..1b217f746e55c2eb9cabd209e35cb232f7a4120b 100644 (file)
--- 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 004a172bad8708ec699dda9a659a97ecb2a05fc1..35c95a3e048a521a059188106117aa551ea8defc 100644 (file)
--- 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 (file)
index 0000000..6d765d5
--- /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;