In reply to foxtrot:
Without an implication, the assertion fails on every negedge clk1 where req does not rise.
With an implication, you get a vacuous pass every time req rises but the sequence for ack does not succeed. That is probably what you want to happen. A non-vacuous pass is required for the assertion to be considered covered.