Chained Implications in SVA

SystemVerilog
, , , , ,
1

I am facing this issue where I need to verify the functionality of an AHB-to-AXI4 bridge and I want to check if the WLAST is properly set using SVAs.

Ultimately, what I want to check in boolean algebra is:

AWVALID && AWREADY → ( 
  (##some-initial-delay0       WVALID && WREADY → !WLAST) and 
  (##longer-delay-after-delay0 WVALID && WREADY →  WLAST) 
)

How can I achieve the same semantics using SV assert property constructs?

I tried the following:

assert property(
    @(posedge clk) disable iff (!rst_n)
        axi4_o.aw.valid && axi4_i.aw.ready
    |-> (##[1:100] (axi4_o.w.valid && axi4_i.w.ready) |-> !axi4_o.w.last)
        ##0 
        (##[1:100] (axi4_o.w.valid && axi4_i.w.ready) |-> axi4_o.w.last)
);

but this does not work since the operand of ##0 must be a sequence not a property and the result of “|->“ is a property.

I ended up later with something like this:

assert_w4: assert property(
    @(posedge clk) disable iff (!rst_n)
        axi4_o.aw.valid && axi4_i.aw.ready
    |-> ##[1:100]((!axi4_o.w.last) throughout (axi4_o.w.valid && axi4_i.w.ready))
        ##[1:100]((axi4_o.w.last) throughout (axi4_o.w.valid && axi4_i.w.ready))
);

But I am not sure if it is equivalent to the intended logic. Any help would be appreciated.

M.E.