Syntax at a glance
$fell(req) |-> ackHow it works
$fell(signal) detects a sampled 1-to-0 transition. For cycles after zero, it is true when the previous sample is one and the current sample is zero. It returns false at cycle zero, including when the signal begins low.
For start = [1, 1, 0, 0, 1, 0], $fell(start) is true at cycles 2 and 5. In $fell(start) |-> pulse, those are the cycles that require pulse. Remaining low at cycle 3 does not create another obligation.
Do not replace a falling-edge trigger with !start. Negation is true at every low sample, so !start |-> pulse would require additional pulses during a long low interval. Similarly, $rose(start) checks the opposite transition and is not interchangeable with $fell(start).
You can require a later reaction by adding delay. $fell(start) |=> pulse requires pulse one sample after each fall. $fell(start) |-> ##2 pulse requires it two samples later. An extra pulse elsewhere is permitted unless another part of the property forbids it.
Only changes visible at sampled clock edges count. The current evaluator does not model X/Z transitions or multibit edge rules. Ensure the trace has enough samples after the last falling edge to complete any delayed obligation, and include both held-low and held-high intervals when testing whether an assertion selects the intended event.