In reply to ben@SystemVerilog.us:
In reply to foxtrot:
Vacuity occurs only if the antecedent $rose(req)==0.
Keep in mind that at every clocking event (i.e., the @(negedge clk1)) you have an attempt at the property, and if in the cycles af$ter the successful $rose(req) you have no more rose, then those attempts are vacuous. Maybe what you see are those vacuous threads.
Right, I have just one rising edge of req now. As I said earlier that solution did not work for me. It’s a vacuous pass even though req and ack are asserted at right time.