Assertions as part of design

Every designer makes assumptions while writing RTL: "this FIFO never overflows because the upstream credit counter prevents it", "these two enables are never high together", "this state is unreachable in normal mode". Those beliefs are exactly the assertions and assumptions formal needs — and they are cheapest to write at the moment they are made.

// Inside RTL: intent captured where it is created
always_ff @(posedge clk) begin
  if (rd_en_a) data_q <= mem_a;
  if (rd_en_b) data_q <= mem_b;      // assumes a and b are never both enabled
end

// ...so say it, right here:
a_rd_exclusive: assert property (@(posedge clk) disable iff (rst) !(rd_en_a && rd_en_b));

A designer's assertion checklist

• Every FSM: legal encoding ($onehot or range) and no illegal transitions.
• Every FIFO / buffer: no overflow, no underflow.
• Every interface: protocol rules on inputs (as assumptions-to-be) and outputs.
• Every "this can't happen" comment: turn it into an assertion.
• Every important corner case: a cover, so you can ask formal to show it.