In reply to ben@SystemVerilog.us:
Hi Ben ,
(1)
I see an ambiguity in the requirement sig2 can only be high for one clock cycle while sig1 is high. Does that mean that there ONE sig2 between $rose(sig1) and ($fell(sig1))?
My interpretation was that only if both sig1 and sig2 are high then , sig2 should be de-asserted at next posedge of clk . Hence I used **$fell( sig2 )** in the consequent
(2) Consider scenario where sig1 is high throughout from posedge T1 to T10 .
My understanding is that Sig2 could be asserted and de-asserted multiple times during this time.
However if we use $rose(sig1) as the antecedent we would miss out on 2nd $rose(Sig2).
(3) Out of curiosity , what is considered the left sequence_expr for intersect operator ?
property prop;
@(posedge clk)
$rose(sig1) |-> sig2[->1] ##1 !sig2[*1:$] intersect sig1[*1:$];
endproperty
Is it **!sig2[*1:$]** OR the entire sequence : **sig2[->1] ##1 !sig2[*1:$] ?**