How do we write assertion for valid to be high while ready is low for AXi protocol

SystemVerilog
1

Hi,

i wrote the below assertion for once valid goes high on any channel, valid to be high while ready is low. lets taks example for write address channel.

assert property @(posedge clk) disable iff (!rst_n)
$rose(a) |-> valid throughout !ready;

but the above passes everytime it sees ready low in next cycle although valid goes low after 2 cycle before ready goes high, it doesnt fail.

can someone please help ?

Thanks,

2

In reply to sv_uvm_learner_1:
You need the throughout a sequence. The “ready” is a sequence of 1 cycle.
The ready[->1] is equivalent to !ready[*0;$] ##1 ready, as long as ready==0.


$rose(a) |-> valid throughout ready[->1];

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
3

In reply to ben@SystemVerilog.us:

  
// A caveat on the use of that **throughout**
// The construct exp throughout seq is an abbreviation for the following: 
(exp) [*0:$] intersect seq
// Your requirements: Once valid goes high on any channel, valid to be high 
// while ready is low.  You did not specify what the value of valid is when ready==1.
// The  valid throughout ready[->1];
// means that when ready==1, valid==1
// If you need to specify that valid==0 when ready==1 
// then you need to use the intersect of 2 sequences. 
 $rose(valid) |-> valid throughout ready[->1]);

 ap_i1: assert property(@ (posedge clk) $rose(valid) |-> !valid[->1] intersect ready[->1]);
 ap_thru1: assert property(@ (posedge clk)   $rose(valid) |-> valid throughout ready[->1]);

http://SystemVerilog.us/vf/thruo_intersect.sv // testbench
http://SystemVerilog.us/vf/intersect.png // simulation

987×541 30.4 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. 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
4

In reply to ben@SystemVerilog.us:

Thanks Ben for quick reply. i was looking for only checking valid to be high while ready is low. once ready goes high in any cycle, valid has to be high and master can drive valid low in that cycle but assertion will capture that in next clock cycle. So, throught assertion is good for me.

between what will be assertion if i want the assertion to be passed irrespective of valid value when ready goes high. in the above assertion, one expect valid should be low and other expect valid to be high to make the assertion pass.

Thanks.

5

In reply to sv_uvm_learner_1:

An assertion is a verification about a property or characteristics of a design.
It reflects the requirements. Sorry, but your last question is unclear in defining the property, the GIGO.
I tend to be very hard on the lack of clarity in defining requirements.
I wrote a book about the chip design and verification process, including a section for the definition of requirements. This book is now free, see
https://verificationacademy.com/forums/announcements/free-book-component-design-example-…-step-step-process-using-vhdl-uart-vehicle