Assertion in AHB( INCR4)

SystemVerilog
,
1

Hello All,
Now i am focused with AHB asertion.
In INCR4 transfer the address will change four times.
If hbusreq signal goes to low, before my haddr should change 4 times.So i am write the assertion below,But it’s not working.

property incr4_addr;
@(posedge hclock) disable iff (hreset == 1’b0)
(htrans==2’h2 && hburst==3’h3) |->(($changed(haddr))[->4]) until_with (hbusreq==0) ;
endproperty

incr4_addr_check : assert property(incr4_addr) else
$error(" incr4 address check failed");

2

It has been a while since I looked at ahb, on the property, do you want
(htrans==2’h2 && hburst==3’h3) |->(($changed(haddr))[->4]) until_with (hbusreq==0) ;
Or
(htrans==2’h2 && hburst==3’h3) |=>(($changed(haddr))[->4]) until_with (hbusreq==0) ;

Also, is the change on the 1st hddr cycle or on subsequent cycles? You have it on the very first cycle.

Many tools provide assertion debug capabilities and show you at what cycle it fails /pass.
Use those tools.
Ben

3

In reply to ben@SystemVerilog.us:

Thnks for replay!
it’s not fail.only fail using the throughout insted of the until_with.
i am using the first one.But it’s not responding means my assertion will finish on the next to hbusreq signal goes to low.And i am changing the 4 haddr to any value my assertion through on error.
(htrans==2’h2 && hburst==3’h3) |->(($changed(haddr))[->4]) until_with (hbusreq==0) ;

Regards
Raja

4

In reply to Rajaraman R:

it’s not fail.only fail using the throughout instead of the until_with.

If you look at the syntax, you have


sequence_expr ::= 
....
| expression_or_dist throughout sequence_expr
| sequence_expr within sequence_expr
...

within : containment of sequences. The within operator defines the containment of a sequence within another sequence.
throughout : The throughout operator is used to check for a Boolean condition to be true during a sequence.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr