In reply to dplumb_amd:
I saw that after the fall of audio_enable the signal codec_dto_base was not repeated.
I consulted with a colleague who is an expert in FV. His take:
I guess that confirms my hypothesis. If stuff can happen between edges of the designated clock, he should modify the assume to act on both edges of the fastest clock : @(fastclk) instead of @(posedge slowclk). Alternatively, SVA also offers the asynchronous reject_on operator if you want to catch such things… but I’m not sure how well tools support this rarely used op.
Ben