Add simple verific VHDL test case

Signed-off-by: Clifford Wolf <clifford@clifford.at>

verific/Makefile

-SUBDIRS = opers sva
+SUBDIRS = opers sva vhdl
 
 all: $(addsuffix /.stamp,$(SUBDIRS))
 	touch .stamp

verific/vhdl/.gitignore

+/.stamp
+/test.log
+/test.status

verific/vhdl/Makefile

+all: test.status
+	grep -H . *.status | sed 's,.status:,\t,; s,PASS,pass,;' | expand -t20
+	touch .stamp
+
+test.status: bar.vhd foo.vhd tb.sv test.ys top.vhd
+	yosys -ql test.log test.ys
+	grep '^SAT .*: SUCCESS' test.log && echo PASS > test.status || echo FAIL > test.status
+
+clean:
+	rm -f test.status test.log .stamp
+
+.PHONY: all clean

verific/vhdl/bar.vhd

+library ieee;
+use ieee.std_logic_1164.all;
+
+entity bar_m is
+	port (
+		clock : in std_logic;
+		a : in std_logic;
+		b : in std_logic;
+		x : out std_logic;
+		y : out std_logic
+	);
+end entity;
+
+architecture rtl of bar_m is
+begin
+	process (clock) begin
+		if (rising_edge(clock)) then
+			x <= a xor b;
+			y <= not (a and b);
+		end if;
+	end process;
+end architecture;

verific/vhdl/foo.vhd

+library ieee;
+use ieee.std_logic_1164.all;
+
+entity foo_m is
+	port (
+		clock : in std_logic;
+		a : in std_logic;
+		b : in std_logic;
+		x : out std_logic;
+		y : out std_logic
+	);
+end entity;
+
+architecture rtl of foo_m is
+begin
+	process (clock) begin
+		if (rising_edge(clock)) then
+			x <= a and b;
+			y <= a or b;
+		end if;
+	end process;
+end architecture;

verific/vhdl/tb.sv

+module tb (input clock, a, b);
+	wire x, y;
+
+	top top_inst (
+		.clock(clock),
+		.a(a), .b(b), .x(x), .y(y)
+	);
+
+	always @(posedge clock) begin
+		assert (x == ($past(a, 2) ^ $past(b, 2)));
+		assert (y == (!$past(a, 2) || !$past(b, 2)));
+	end
+endmodule

verific/vhdl/test.ys

+verific -work foo -vhdl foo.vhd
+verific -work bar -vhdl bar.vhd
+verific -vhdl top.vhd
+verific -import top
+read_verilog -sv tb.sv
+prep -flatten -top tb
+sat -prove-asserts -prove-skip 5 -seq 10 -show-all tb

verific/vhdl/top.vhd

+library ieee;
+use ieee.std_logic_1164.all;
+
+library foo;
+use foo.foo_m;
+
+library bar;
+use bar.bar_m;
+
+entity top is
+	port (
+		clock : in std_logic;
+		a : in std_logic;
+		b : in std_logic;
+		x : out std_logic;
+		y : out std_logic
+	);
+end entity;
+
+architecture rtl of top is
+	component foo_m is
+		port (
+			clock : in std_logic;
+			a : in std_logic;
+			b : in std_logic;
+			x : out std_logic;
+			y : out std_logic
+		);
+	end component;
+	component bar_m is
+		port (
+			clock : in std_logic;
+			a : in std_logic;
+			b : in std_logic;
+			x : out std_logic;
+			y : out std_logic
+		);
+	end component;
+	signal t1, t2 : std_logic;
+begin
+	foo_inst : foo_m port map (
+		clock => clock,
+		a     => a,
+		b     => b,
+		x     => t1,
+		y     => t2
+	);
+
+	bar_inst : bar_m port map (
+		clock => clock,
+		a     => t1,
+		b     => t2,
+		x     => x,
+		y     => y
+	);
+end architecture;