Syntax at a glance
b == $past(a)How it works
Equality checks whether two Boolean values are the same at a sampled cycle. Both 0 == 0 and 1 == 1 are true; 0 == 1 and 1 == 0 are false. A standalone equality property must be true at every sample in the trace.
For b == $past(a), b must reproduce the previous sample of a, including its zeros. If a = [1, 0, 1, 1], the matching b trace is [0, 1, 0, 1]. The initial zero comes from the lab's missing-history rule. A b pulse in a cycle where the previous a was zero makes this equality fail.
Compare this with a |=> b. That implication only requires a high b after a high a; it does not forbid b when the previous a was zero. Equality therefore captures a stronger, two-way relationship than that one-way implication. Choose the expression that matches the requirement.
Equality can be conditional too: enable |-> (a == b) compares the pair only during enabled cycles. You may also compare Boolean expressions, for example (a && b) == ready. Parentheses help show which expressions are being compared.
This evaluator compares binary Boolean values. It does not model X/Z states, case equality, vectors, widths, or signed numeric comparisons. Equality binds more tightly than && and || here. When expressing stability as data == $past(data), remember that at cycle zero equality uses the zero history value, while $stable(data) is explicitly false at cycle zero.