Hi Dave and Ben,
I went through the discussion in the threads. Understood that the $rose(write_cycle) is being sampled in the preponed region and evaluated in the observed region, hence the behaviour. I am not trying to modify any DUT signal in the assertion. match_found is Not a DUT signal but a verification support signal whose scope is limited to the checker block in which the assertion is written. Actually the entire code is written inside a checker block. Extremely sorry for not being able to convey my intent clearly. Below is my intent.
Bit write_cycle goes HIGH whenever an APB write cycle is detected. When a write_cycle is detected, within 0 to 2 APB clocks first match occurs according to the comparison statement written inside first_match() construct. So when the first match occurs a bit match_found is set HIGH. This match_found bit remains HIGH until the next write_cycle is detected. On detection of a write_cyle the match_found is reset. Also this match_found bit is used in a always_comb to check that comparison which was written inside the first_match() remains valid until the next write_cycle is detected.
The code that I had written is as follows:
($rose(write_cycle),reset_match_found()) |-> ##[0:2] (first_match(/*comparision statement*/),set_match_found());
function void reset_match_found();
match_found = 0;
match_found = 1;
if (/*comparison statement is invalid*/)
The intent of using an always_comb block is to ensure the comparison happens independent of any clock.