Add some simple SVA test cases for future Verific work

[yosys.git] / tests / sva / basic01.sv

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