AXI assertion question

SystemVerilog
,
1

I am writing an assertion for the following scenario, however i noticed it is not working as intended. can somebody tell me what is wrong here? the assertion doesnt fail when awvalid deasserts one clock cycle before. Also i would like to see the assertion being written with until and throughout.

From AXI spec,
when AWVALID is asserted, then it remains asserted until AWREADY is high.



 property AXI4_ERRM_AWVALID_STABLE;
    @(posedge aclk) disable iff (!areset_n) 
          $rose(awvalid) |-> ((awvalid)[*1:$] intersect (awready));
  endproperty
2

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/ ben@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 SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:
3

In reply to ben@SystemVerilog.us:

Thanks Ben !

4

This is a reply to another post.
https://verificationacademy.com/forums/systemverilog/assertion-axi

It has been many years since I looked at the AMBA AXI stuff, thus I cannot go into specifics.
Here are comments and a suggestion that I hope will be helpful.

Your assertion does not a precondition (an antecedent) to start the needed tests.
In 2004 I addressed the AMBA as an example in my PSL book, and I wrote many assertions for that interface. Whether I would write them in the same manner today is debatable. I also DO NOT recommend the use of PSL, as SVA is IMHO far better and more mature.
I am giving you a copy of that chapter and the code. SVA has a lot of similarities to PSL and you should be able to get some inspirations into possible assertions.

http://systemverilog.us/vf/ch8.zip
Best wishes,
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy