Always property in assertions

SystemVerilog
, , ,
2

In reply to nipradee:

I’ve never seen always used in the antecedent of an implication. To be true, req must remain high forever. You may be confusing SVA with PSL assertions. They are two different syntaxes.

I think what you want to write is

property (@posedge clk) disable iff (reset)
          $rose(request) |=> request s_until grant;
endproperty

This says for each request, request must remain high until grant, which must happen.