I have a question about first_match() usage in concurrent assertions.
There is a scenario, where upon satisfying a condition (say sig1 && !sig2), sig3[1:0] is supposed to be 01 after four clock cycles. I have written the property as below:
@(posedge clk) disable iff(reset)
(sig1 && !sig2) |-> (##4 (sig3 == 2'b01));
This is working fine, and the assertion is passing after 4 clock cycles when both the conditions are met (antecedent true at 1st cycle, consequenct at 5th cycle). But the issue is that the antecedent holds true in 2nd, 3rd, 4th clock cycles also but consequent doesn't need to be true in 6th, 7th, 8th cycles and because of which, I see false assertion failures.
To avoid this, I have enclosed antecedent in first_match() operator, but it is not working.
I tried first_match with the consequent too and it doesn't work either.
Let me know if my understanding of first_match() is correct or wrong. If correct, I'd follow up with tool vendor on this. If wrong, please suggest the best method to resolve this.
PS: Note that I can't use $rose(sig1) or $fell(sig2) as such as there is no certain order of whether sig1 roses first or sig2 falls first. It depends on the configuration.