When enable == 1 I have to check that b is down once time at least when another signal a is high.
I wrote it with a counter, checking that it’s different from zero when enable goes down.
Is there a simpler way to implement this assertion?
In reply to ben@SystemVerilog.us:
Hi Ben,
Does your solution restrict the check to the same cycle as enable signal rose or would it span multiple cycles until the first occurrence of $fell(b)?
Somehow, with the overlapping implication, I am misled into believing this wont work as intended. Could you kindly clarify?
(seq1 within seq2) // is equivalent to:
((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 ) //Thus,
a |-> b within c[->1]; // equivalent to
a |-> ((1[*0:$] ##1 b ##1 1[*0:$]) intersect
!c[*0:$] ##1 c)
// if a==1, b==1, c==1 then for that attempt, above expression gets reduced to
a|-> ( b ##1 1[*0:$]) intersect c; / or simply
a |-> b inteeset c; // true in that attempt.
// Now, for your case
$rose(enable) |-> $fell(b) && a within $fell(enable)[->1]);
// You CANNOT have a $rose(enable) and a $fell(enable) in the same cycle, thus
// the check would span over multiple cycles until the first occurrence of $fell(b)?
// However, the following can occur in the same cycle since the $rose and $fell can occur in //the same cycle
$rose(enable) |-> $fell(b) && a within $fell(c)[->1]);