Assertions

Assertions turn rules into executable checks. They catch protocol bugs near the source and document intent for readers.

Immediate assertions

Checked when the procedural statement runs (typically in a TB or always_comb/always_ff with care):

always_ff @(posedge clk) begin
  if (valid) assert (!$isunknown(data))
    else $error("data X when valid");
end

Concurrent assertions (SVA sketch)

Sampled on a clock edge; good for protocols:

assert property (@(posedge clk) disable iff (!rst_n)
  valid && ready |=> !valid || data_stable
);

(Exact sequences depend on your bus — treat this as a shape, not a drop-in.)

Assert vs assume vs cover

Where to put them

• Interfaces / protocol checkers — reusable
• Beside FSM defaults — illegal state
• TB — end-to-end properties

Keep synthesizable DUT free of TB-only assertion libraries if your synth flow chokes — use `ifdef or separate bind files when needed.

Start small

1. No X on payload when valid
2. Mutual exclusion (!$onehot0(grants))
3. Handshake: no drop while valid && !ready (per spec)

Grow into full SVA in the SystemVerilog / UVM learn tracks.