Immediate Assertions and SVA

Check a local condition, express a rule across cycles, and disable properties cleanly during reset.

An assertion for one precise rule

An assertion reports when an assumed condition is false. It does not replace a scoreboard. It mainly checks invariants, protocol rules, and local temporal relationships.

An immediate assertion is evaluated when procedural code reaches it.

always_comb begin
  assert (!$isunknown({i_valid, i_ready}))
    else $error("Handshake contains X or Z");
end

It fits a combinational condition or a check inside a task. It does not retain history across cycles.

A temporal property

SVA expresses a relationship between events sampled on a clock.

property request_gets_response;
  @(posedge i_clk) disable iff (i_rst)
    i_request |-> ##[1:4] o_response;
endproperty
 
assert property (request_gets_response)
  else $error("No response within four cycles");

|-> is overlapped implication. If i_request is true at the starting cycle, the consequent begins on that same cycle. The ##[1:4] delay then requires o_response one to four cycles later.

With |=>, the consequent begins on the next cycle. The choice must match the protocol exactly.

Stability under backpressure

A valid/ready protocol often requires data to remain stable while valid is 1 and ready is 0.

property hold_data_while_stalled;
  @(posedge i_clk) disable iff (i_rst)
    i_valid && !i_ready |=> i_valid && $stable(i_data);
endproperty
 
assert property (hold_data_while_stalled);

This property checks the cycle after every stalled cycle. Depending on the protocol, other fields such as last, address, or byte enables may also need stability checks.

Reset and unknown values

disable iff (i_rst) abandons active attempts and disables the property during reset. Polarity and synchronous or asynchronous behavior must match the design.

An assertion can pass vacuously when its antecedent never occurs. A related cover property shows that a scenario was observed:

cover property (@(posedge i_clk) disable iff (i_rst)
  i_request ##[1:4] o_response);

Keep properties readable

A short property with a clear name is easier to maintain than one long expression. First write the rule in plain language, define the starting cycle, and sketch two or three timing diagrams before coding it.

Key points

• An immediate assertion checks a condition at its execution point.
• A concurrent assertion samples a relationship over time.
• |-> and |=> do not start the consequent on the same cycle.
• disable iff handles active attempts during reset.
• A property can pass without being exercised, which makes coverage useful.

📝 Test your knowledge - Chapter quiz