Hi Ben,
(A) The requirement at the top of this thread mentions
A is going down for 100ns.
B toggle 20 times, only when A in low.
I need to check that the last edge of B happens at least 20ns before A go to high.
As we want to check that ‘b’ should toggle 20 times when ‘a’ is low,
shouldn’t we check for ‘b’ in lhs of intersect operator ?
property p;
realtime v;
int count;
@(posedge clk) ($fell(a), v=$realtime, count=0) |->
(@(clk) <seq_expr_involving_b>[*1:$] intersect a[->1]) ##0 $realtime - b_now == 20ns ##0 count==20;
endproperty
The requirement that ‘b’ should toggle 20 times when ‘a’ is low has 2 possible interpretations
(1) Change in ‘b’ is is checked on each posedge of clk
(2) Change in ‘b’ is is detected asynchronously
Limitation with (1) is that if ‘b’ were to toggle twice b/w 2 posedges of clk Tx & Ty,
sampled value of ‘b’ at Ty would be same as the previous clock Tx (as ‘b’ changed twice)
I feel a more robust solution would be (2) as it detects transition in ‘b’ between 2 clock edge as well
(B)
I found an older post where the logical reasons behind legality are mentioned.
For multiclocked ‘intersect’, it’s acceptable if the lhs & rhs sequence start at different clocks (similar to multiclocked ‘and’)
However, the issue with multiclocked ‘intersect’ is that the ending of the 2 sequences can’t be guaranteed with non-identical clocks (for multiclocked ‘and’ the 2 sequences could end at different clocks)