SystemVerilog Assertions: Once A is asserted, A remains high until B is de-asserted, and after that A will finally be low

Question

I tried to write a assertion:

Once A is asserted, A remains HIGH until B is de-asserted. After that, A will finally de-asserted.

The assertion I wrote was:

my_assertion : assert property(
    @(posedge clk) disable iff(reset)
    $rose(A) |-> A throughout !B [->1] ## [0:$] !A) 
else $display("Assertion failed") 

The assertion failed at the time when A is de-asserted. Guys, can you please tell me where I did wrong in my_assertion? Was " [0:$] " not used correctly?

Answer 1

## has a higher priority than throughout; See IEEE1800-2012 § 16.9 Sequence operations Table 16-1.

Therefore A throughout !B [->1] ## [0:$] !A is the sample a A throughout (!B [->1] ## [0:$] !A). This fails because A is required be high (left side of throughout) and low (right side of throughout) for the last cycle, which will always evaluate as false.

I believe the desired behavior is: (A throughout !B [->1]) ## [0:$] !A