While a sequence defines a pattern of events, a property defines the actual "rule" that must be valid. Properties encapsulate sequences, implications, and clocking/reset conditions.
A property typically specifies three things:
@(posedge clk)property p_safe_grant;
@(posedge clk)
disable iff (!rst_n) // Ignore checking when Reset is Active Low
req |=> gnt; // The Rule
endproperty
a_safe_grant: assert property (p_safe_grant);
The disable iff clause is critical. During reset, signals are often
indeterminate.
If you don't disable assertions, you will get a flood of "X state" errors or protocol
violations
during the reset phase.
disable iff (!rst_n) in your
properties unless the check is strictly required during reset.
You can check that something should NEVER happen using the not
keyword.
property p_no_conflict;
@(posedge clk) disable iff (!rst_n)
// "It should NEVER be the case that we write and read same addr simultaneously"
not (write && read && (w_addr == r_addr));
endpropertydisable iff (Disable If and Only If) is an asynchronous kill-switch for the
property. If the condition is true, the current evaluation is aborted. Standard
if logic is part of the property expression itself.
disable iff is preferred for resets.