Add more SVA test cases for future Verific work

5 files changed, 74 insertions, 1 deletions

diff --git a/tests/sva/basic02.sv b/tests/sva/basic02.sv
index 6100c50ae..cf2d72ae7 100644
--- a/tests/sva/basic02.sv
+++ b/tests/sva/basic02.sv
@@ -13,4 +13,4 @@ module top_properties (input logic clock, read, write, ready);
 	a_wr: assert property ( @(posedge clock) write |-> ready );
 endmodule
 
-bind top top_properties inst (.*);
+bind top top_properties properties_inst (.*);
diff --git a/tests/sva/basic04.sv b/tests/sva/basic04.sv
new file mode 100644
index 000000000..6f02f3c19
--- /dev/null
+++ b/tests/sva/basic04.sv
@@ -0,0 +1,6 @@
+module top_properties (input logic clock, read, write, ready);
+	a_rw: assert property ( @(posedge clock) !(read && write) );
+	a_wr: assert property ( @(posedge clock) write |-> ready );
+endmodule
+
+bind top top_properties properties_inst (.*);
diff --git a/tests/sva/basic04.vhd b/tests/sva/basic04.vhd
new file mode 100644
index 000000000..889bef0d2
--- /dev/null
+++ b/tests/sva/basic04.vhd
@@ -0,0 +1,26 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity top is
+	port (
+		clock : in std_logic;
+		ctrl : in std_logic;
+		x : out std_logic
+	);
+end entity;
+
+architecture rtl of top is
+	signal read : std_logic;
+	signal write : std_logic;
+	signal ready : std_logic;
+begin
+	process (clock) begin
+		if (rising_edge(clock)) then
+			read <= not ctrl;
+			write <= ctrl;
+			ready <= write;
+		end if;
+	end process;
+
+	x <= read xor write xor ready;
+end architecture;
diff --git a/tests/sva/basic05.sv b/tests/sva/basic05.sv
new file mode 100644
index 000000000..03854aaac
--- /dev/null
+++ b/tests/sva/basic05.sv
@@ -0,0 +1,15 @@
+module top (input logic clock, ctrl);
+	logic read, write, ready;
+
+	demo uut (
+		.clock(clock),
+		.ctrl(ctrl)
+	);
+
+	assign read = uut.read;
+	assign write = uut.write;
+	assign ready = uut.ready;
+
+	a_rw: assert property ( @(posedge clock) !(read && write) );
+	a_wr: assert property ( @(posedge clock) write |-> ready );
+endmodule
diff --git a/tests/sva/basic05.vhd b/tests/sva/basic05.vhd
new file mode 100644
index 000000000..930f1ba22
--- /dev/null
+++ b/tests/sva/basic05.vhd
@@ -0,0 +1,26 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity demo is
+	port (
+		clock : in std_logic;
+		ctrl : in std_logic;
+		x : out std_logic
+	);
+end entity;
+
+architecture rtl of demo is
+	signal read : std_logic;
+	signal write : std_logic;
+	signal ready : std_logic;
+begin
+	process (clock) begin
+		if (rising_edge(clock)) then
+			read <= not ctrl;
+			write <= ctrl;
+			ready <= write;
+		end if;
+	end process;
+
+	x <= read xor write xor ready;
+end architecture;