SVA for AHB protocol violations - Read bus should not get data when write transaction is going on

SystemVerilog
,
1

Hi All,

I have written an assertion to check the AHB protocol violation.

The scenario is like below.

  • While doing write transaction, slave should not send any data on read data bus.
    The assertion is like below.

    assert_prop : assert property (@(posedge clk) disable iff (rst) (hsel & hwrite) ##[1:$] hready |-> (hrdata == 'h0))
    else
    $error(“Assertion error”);

I am facing an issue with the above assertion, it is throwing error only for the first time when the assertions fails, but not later failures.

Please suggest to overcome the issue so that whenever the violations happens it prints error.

Thank you,
Sanjoy Saha

2

In reply to sanjay864u:

Sanjay,
It’s happening due to 1:$ in the antecedent. What you need is something like below:


  vw_no_rd_during_wr : assert property (@(posedge clk) disable iff (rst) 
   (hsel & hwrite && hready |=> $stable(hrdata)
   else
     `uvm_error("CIP", "hrdata changed during a write transfer");

HTH
Srini
www.verifworks.com

3

In reply to Srini @ CVCblr.com:

Hi Srini Sir,

I have a few queries on the above code.

  1. I did not get the use of logical and bit wise and operation.
    hsel & hwrite && hready

  2. Also, if the slave does not return the HREADY at the very next cycle after HSEL and HWRITE, then how the above part of code will work? It may happen the slave is not ready to take the HWDATA.

Thanks & regards,
sanjoy

4

In reply to Srini @ CVCblr.com:

Hi Srini Sir,

I have used the property you have suggested but there also only first time the error is getting printed.

Thanks & regards,
sanjoy

5

In reply to sanjay864u:
Hello Sanjoy
When there is write on the bus , and hready can go high in certain delay. when it goes high hrdata should be zero.


 vw_no_rd_during_wr : assert property (@(posedge clk) disable iff (rst) 
   (hsel & hwrite) |-> hrready[->1] ##0 (hrdata==0);
   else
     `uvm_error("CIP", "hrdata changed during a write transfer");
6

In reply to kddholak:

Hi,

With the below code the assertion did not fail for a single time also.

vw_no_rd_during_wr : assert property (@(posedge clk) disable iff (rst)
(hsel & hwrite) |-> hrready[->1] ##0 (hrdata==0);
else
`uvm_error(“CIP”, “hrdata changed during a write transfer”);

thanks & regards,
sanjoy

7

In reply to sanjay864u:

Sanjay,
As far as I recall in AHB, control signal like heel, write shall remain constant during wait state, hence my simple logic of:

hsel && hwrite && hready

Should work in this case. And I suggest you use logical AND only, though in this example it may not make a difference (See: Verification Course Blog | VeriLog Courses | CVC).

I used $stable(hrdata) as I don’t recall AHB spec saying rdata shall be ZERO during write transfer - do you have a spec pointer for this?

Regards
Srini
www.verifworks.com

8

In reply to Srini @ CVCblr.com:

Hi Srini Sir,

The HSEL and HWRITE remain constant in case of address phase, once the address is decoded the HREADY may go low from slave and prolong the data phase.

And $stable(hrdata) is fine as per spec, I used (hrdata==0) for my application purpose.

thanks & regards,
sanjoy

9

In reply to sanjay864u:

Yes, for the address phase my above code should do the job for you. For extended data phases (waits, splits etc.) you will need some custom logic to indicate pending wait_xfer and use that signal in a similar property.

HTH
Srini
www.verifworks.com

10

In reply to sanjay864u:

According to AHB specification, value on HRDATA does not matter when WRITE transaction is going on. This assertion might be fine with your design, but it’ll throw unnecessary errors with other AHB compliant designs.

11

In reply to MayurKubavat:

Hi Mayur,

As per AHB spec, HRDATA should be stable during WRITE transaction as Srini Sir mentioned in last comment.
If it happens then it is a protocol violation.
Moreover, in case of protected transfer if this happens the the protected data may come to the bus which hackers can easily get.
This kind of checks must be present in AHB AVIP.

thanks & regards,
sanjoy