Add simple VHDL+PSL example

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;