Syntax at a glance
b == $past(a, 2)How it works
$past(signal) reads that signal one sampled cycle before the current cycle. $past(signal, N) reads N cycles back. This is a historical value lookup, not a request to move the consequent into the future. The argument must be a signal name in the lab's subset.
If a = [1, 0, 1, 1], then $past(a) produces [0, 1, 0, 1], while $past(a, 2) produces [0, 0, 1, 0]. Missing history is defined as zero. $past(a, 0) reads a at the current sample. History values must be integers from 0 to 128.
Use b == $past(a) when b must exactly reproduce the previous a, including zeros. Use $past(a) |-> b when you only want to require b after a previously high a. The latter permits extra b pulses because it has no obligation when the historical value is zero.
History is evaluated where its expression is checked. For req |-> ##2 (ack == $past(a)), the comparison occurs at t+2, so $past(a) refers to a at t+1. It does not refer to the sample before the original request.
Be deliberate about initialization. At cycle zero, data == $past(data) is true if data is zero, but $stable(data) is always false there in this lab. They agree about unchanged values only once history exists. A delayed equality and an implication may look similar on one waveform while classifying other behaviors differently.