Concurrent assertion to check address with previously sampled value on every clk edge

SystemVerilog
1

Hi,
Want a systemverilog assertion which checks address with previously sample address in local variable on every clk edge until certain condition occurs.
Here i have written assertion but it is not checking address on every posedge of clk.

property priority_over_read_txn;
logic [40:0] observed_addr;
@(negedge clk_1) ((q_full & vld & rdy), observed_addr = addr) |-> @(negedge clk_2) ((cha_addr !== observed_addr) & q_full & cmd_valid[=1:$]) ##1 !q_full;
endproperty

Can anyone suggest how can we use “until” here or is there any other way to write assertion for this scenario?

Thank you.
Piyush

2

In reply to ben@SystemVerilog.us:

Hi Ben,

Thank you for your suggestions and clear explanation.
Able to produce correct assertion using your s_until example.

Below assertion is working for me.

property priority_over_read_txn;
logic [40:0] observed_addr;
@(negedge clk_1) ((q_full & vld & rdy), observed_addr = addr) |->
@(negedge clk_2 && cmd_valid) ((cha_addr !== observed_addr) && q_full) s_until !q_full;
endproperty

Thank you.
Piyush