Concurrent Assertions (SVA)

Properties and sequences that check protocol rules on every clock edge: |->, |=>, ##, $rose and disable iff.

Concurrent assertions describe behaviour over time: 'after a request, a grant must arrive within 3 cycles'. They are evaluated on every clock edge for the whole simulation, catch protocol violations at the exact cycle they happen, and can be proved mathematically by formal verification tools.

Checking a request/grant protocol

$rose(req) |-> ##[1:3] gnt: when req rises, gnt must be high 1 to 3 clocks later.

gnt |-> req: in the same cycle as a grant there must be a request (overlapping implication).

gnt |=> busy: the cycle after a grant, busy must be high (non-overlapping implication).

disable iff (rst): the checks are switched off during reset.

The SVA building blocks

assert property (@(posedge clk) req |-> gnt); // during reset too assert property (@(posedge clk) disable iff (rst) req |-> ##[1:3] gnt);

Without disable iff, signals in reset (or X before reset) produce false failures. And check the timing your protocol really allows.

Write a property: after valid rises, data must stay stable until ready is high.

@(posedge clk) disable iff (rst) (valid && !ready) |=> $stable(data);

Is a |=> b the same as a |-> ##1 b?

Yes. Non-overlapping implication is shorthand for overlapping implication followed by a one-cycle delay.