diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-07-22 12:31:08 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-07-22 12:31:08 +0200 |
| commit | 024ba310ecffa9dde47bbe66d82eab91d1f0c609 (patch) | |
| tree | 3288787070ef5ca48411fef6459b863aaac82eee /tests/sva/basic02.sv | |
| parent | 2785aaffeb66575128da1f68044dd317660e0f3b (diff) | |
| download | yosys-024ba310ecffa9dde47bbe66d82eab91d1f0c609.tar.gz yosys-024ba310ecffa9dde47bbe66d82eab91d1f0c609.tar.bz2 yosys-024ba310ecffa9dde47bbe66d82eab91d1f0c609.zip | |
Add some simple SVA test cases for future Verific work
Diffstat (limited to 'tests/sva/basic02.sv')
| -rw-r--r-- | tests/sva/basic02.sv | 16 |
1 files changed, 16 insertions, 0 deletions
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 (.*); |