Add some simple SVA test cases for future Verific work

4 files changed, 45 insertions, 0 deletions

diff --git a/tests/sva/basic00.sv b/tests/sva/basic00.sv
new file mode 100644
index 000000000..387f3deef
--- /dev/null
+++ b/tests/sva/basic00.sv
@@ -0,0 +1,7 @@
+module top (input clk, reset, antecedent, output reg consequent);
+	always @(posedge clk)
+		consequent <= reset ? 0 : antecedent;
+
+	test_assert: assert property ( @(posedge clk) disable iff (reset) antecedent |-> consequent )
+			else $error("Failed with consequent = ", $sampled(consequent));
+endmodule
diff --git a/tests/sva/basic01.sv b/tests/sva/basic01.sv
new file mode 100644
index 000000000..596e48db0
--- /dev/null
+++ b/tests/sva/basic01.sv
@@ -0,0 +1,12 @@
+module top (input logic clock, ctrl);
+	logic read = 0, write = 0, ready = 0;
+
+	always @(posedge clock) begin
+		read <= !ctrl;
+		write <= ctrl;
+		ready <= write;
+	end
+	
+	a_rw: assert property ( @(posedge clock) !(read && write) );
+	a_wr: assert property ( @(posedge clock) write |-> ready );
+endmodule
diff --git a/tests/sva/basic02.sv b/tests/sva/basic02.sv
new file mode 100644
index 000000000..6100c50ae
--- /dev/null
+++ b/tests/sva/basic02.sv
@@ -0,0 +1,16 @@
+module top (input logic clock, ctrl);
+	logic read = 0, write = 0, ready = 0;
+
+	always @(posedge clock) begin
+		read <= !ctrl;
+		write <= ctrl;
+		ready <= write;
+	end
+endmodule
+
+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 inst (.*);
diff --git a/tests/sva/basic03.sv b/tests/sva/basic03.sv
new file mode 100644
index 000000000..a15f3f3a4
--- /dev/null
+++ b/tests/sva/basic03.sv
@@ -0,0 +1,10 @@
+module top (input logic clk, input logic selA, selB, QA, QB, output logic Q);
+	always @(posedge clk) begin
+		if (selA) Q <= QA;
+		if (selB) Q <= QB;
+	end
+
+	check_selA: assert property ( @(posedge clk) selA|=> Q == $past(QA) );
+	check_selB: assert property ( @(posedge clk) selB|=> Q == $past(QB) );
+	assume_not_11: assume property ( @(posedge clk) !(selA& selB) );
+endmodule