Syntax at a glance
$rose(req) |-> ackHow it works
$rose(signal) detects a sampled 0-to-1 transition. At cycle t greater than zero, it is true only when the previous value was zero and the current value is one. At cycle zero, it returns false because there is no previous sample.
For start = [0, 1, 1, 1, 0, 1], $rose(start) is true at cycles 1 and 5 only. The held-high samples at cycles 2 and 3 are not new rising edges. In $rose(start) |-> pulse, pulse is required at those two transition cycles; extra pulse samples are allowed.
Compare start |-> pulse. That version requires pulse on every high start sample, including cycles 2 and 3. It is too restrictive if the requirement only mentions rising edges. Conversely, an edge-triggered property can be too permissive when the requirement really applies to every high sample.
Edges combine naturally with temporal windows: $rose(req) |-> ##[1:3] ack creates one response-window obligation per rising transition. It does not continuously restart the window while req stays high. If req falls and rises again, that later edge creates its own obligation.
This is sampled transition detection. It does not observe unsampled changes between clock edges, and the lab only supports binary values. An initially high signal is not treated as a rising edge. Include a preceding zero sample in a teaching trace when you want to demonstrate a first visible rise.