This is a micro post about an example of a handshake SystemVerilog assertion. This is more of a diary thing, so take it with a grain of salt.

Assertion Details Link to heading

After a req edge, req should be stable and ack should be low until ack goes high between 0:11.

$rose(req) |-> (req && !ack)[*0:11] ##1 (req && ack)

When ack goes high, req should be high as well.

!req |-> !ack

req goes low after ack goes low.

$fell(req) |-> !ack