Add some simple SVA test cases for future Verific work

diff --git a/tests/sva/basic00.sv b/tests/sva/basic00.sv
new file mode 100644 (file)
index 0000000..387f3de
--- /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 (file)
index 0000000..596e48d
--- /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 (file)
index 0000000..6100c50
--- /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 (file)
index 0000000..a15f3f3
--- /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