Showing results for 
Show  only  | Search instead for 
Did you mean: 
Registered: ‎11-28-2013

Understanding the AXI protocol handshake properties expressed with SystemVerilog

The ARM AXI protocol checker documentation describes illegal states of the use of AXI transaction, such as handshakes for the write address channel, the read data channel, etc. For example, the checks for violation for the write address channel handshaking is here:


ARM provides AXI protocol monitor IP as open source SystemVerilog properties that watch the signals relevant to each transaction. For example one such SystemVerilog property is:


@(posedge `AXI4_SVA_CLK) disable iff (PROTOCOL != `AXI4PC_AMBA_AXI4)
  !($isunknown({AWVALID,AWREADY,AWADDR})) &
  ##1 `AXI4_SVA_RSTn
  |-> $stable(AWADDR)

An interpretation of this is:


This property is tested if the current Protocol is  AXI4PC_AMBA_AXI4. The property asserts that AWADDR must remain stable if none of these signals is unknown (AWVALID,AWREADY,AWADDR), AXI4_SVA_RSTn  and AWVALID signals are '1'  and AWREADY signal is '0' in the first clock cycle, and AXI4_SVA_RSTn remains '1' in the next clock cycle.


A violation of this property will produce the error message:


"AWADDR must remain stable when AWVALID is asserted and AWREADY low. Spec: section A3.2.1."


My two questions are these:


1. Is this an accurate interpretation?


2. Why is it only important that the AXI4_SVA_RSTn signal remains 1 over this and the successive clock cycle (the ##1 part), rather than the whole precondition in the |-> implication? I.e. Why is the property not:


@(posedge `AXI4_SVA_CLK) disable iff (PROTOCOL != `AXI4PC_AMBA_AXI4)
      !($isunknown({AWVALID,AWREADY,AWADDR})) &
      ($isunknown({AWVALID,AWREADY,AWADDR})) &
      |-> $stable(AWADDR);


0 Kudos
1 Reply
Registered: ‎08-01-2012

1. Yes.
2. if Reset is asserted, then the sequence wont hold, no matter what AWVALID and AWREADY are in the next cycle, and the assertion wont be checked.
If the reset remains de-asserted, then a new assertion will be triggered to ensure stability.
checking SVA can be quite CPU intensive, so reducing the complexity is always a good idea.

BTW, these same assertions hold for ALL AXI channels.