In AXI VALID/READY Handshake we have 3 scenarios how to write Assertion

SystemVerilog
, , , ,
1

In AXI we know we have VALID/READY handshake to transfer data and control information. Transfer occurs only when both the VALID and READY signals are HIGH, but here we have 3 scenarios when the transfer happens and below are assertion we may have

  1. Valid Before Ready

property valid_B_rdy ;
@(posedge clk) $rose(valid) |=> $rose(ready);
endproperty
  1. Ready Before Valid

property rdy_B_valid ;
@(posedge clk) $rose(ready) |=> $rose(valid);
// $rose(ready) |=> [0:3] $rose(valid) if "ready" is initially 1 during simulation and  valid take some time to get asserted
endproperty
  1. Valid with Ready

property valid_w_rdy ;
@(posedge clk) $rose(valid) |-> $rose(ready);
endproperty

So during our formal verification check… any of above scenarios can happen. Can we write assertion such that tool will say which property has been asserted during simulation and print statement like “Property valid_w_rdy is successful” &
Can i writing my code to check 3 scenarios at one go as below ? correct me if it is wrong


a1: assert property (valid_B_rdy or rdy_B_valid or valid_w_rdy) else $error("AXI HANDSHAKE NOT HAPPEN")
1 Like
2

In reply to SUNODH:
Your assertion with the ORing is ok.
Extracting which property has been asserted is problematic. I thought of the following solution where each of the properties calls a function with an ID upon a true. That function asserts an event based on the ID. In theory, it should work. In practice, the simulator optimizes out the evaluation of other properties on a pass of one property, thus I don’t get all the flags.
The complete model is AT http://systemverilog.us/vf/theoring.sv
The best solution for simulation is to assert the individual properties and add action blocks. The failures can be ignored. Basically, those 3 assertions would be more for debug.


event e1, e2, e3; 
     function automatic void flag(int a);
         case (a)
             0: -> e1; 
             1: -> e2; 
             2: -> e3; 
         endcase
     endfunction
  
    property p_a;  
      @(posedge clk)   a |-> (b, flag(0));
     endproperty 

     property p_b;  
      @(posedge clk)   b |-> (a, flag(1));
     endproperty 

     property p_c;  
      @(posedge clk)   a |=> (b, flag(2));
     endproperty 
     ap_all: assert property(p_a or p_b or p_c);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

1 Like