In reply to rag123:
[spec]When asserted, AWVALID must remain asserted until the rising clock edge after the slave asserts AWREADY
.. the slave can assert AWREADY before AWVALID or WVALID, or both, are asserted
[Ben] Do we need the $rose(AWVALID) ?
property AXI4_ERRM_AWVALID_STABLE;
@(posedge aclk) disable iff (!areset_n)
$rose(awvalid) |->
strong(awvalid[*1:$] intersect awready[->1); // need the goto
endproperty
property AXI4_ERRM_AWVALID_STABLE2;
@(posedge aclk) disable iff (!areset_n)
$rose(awvalid) |-> awvalid s_until_with awready;
endproperty
Ben Cohen
http://www.systemverilog.us/
For training, consulting, services: contact
http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats
https://rb.gy/a89jlh
2) Free books: Component Design by Example
https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3)
https://rb.gy/cwy7nb
3) Papers:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
